HomeIsabelle/Phabricator

added lemma reflp_on_reflclp[simp]