HomeIsabelle/Phabricator

added lemmas reflp_on_subset, totalp_on_subset, and total_on_subset