HomeIsabelle/Phabricator

introduced predicates irrefl_on and irreflp_on, and redefined irrefl and…