HomeIsabelle/Phabricator

added lemmas irrefl_on_subset and irreflp_on_subset