HomeIsabelle/Phabricator

added lemma ex_mgu_if_subst_apply_term_eq_subst_apply_term