HomeIsabelle/Phabricator

added lemma totalp_on_converse[simp]