HomeIsabelle/Phabricator

added lemma wfP_subset_mset[simp]