HomeIsabelle/Phabricator

added lemma subst_apply_term_eq_subst_apply_term_if_mgu