HomeIsabelle/Phabricator

added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]