proposition: Lemma unify_unifiable E sigma: E ↦ sigma -> Unifies sigma E.
proof: Proof. induction 1. - eapply equi_unifiable_decomp' in H. eapply H; easy. - eapply equi_unifiable_decomp' in H. eapply H. eapply equi_unifiable_cons. eapply Unifies_cons; cbn; intuition idtac. + unfold unifies; cbn. unfold update at 1; destruct eq_dec. 2:easy. symmetry; erewrite subst_extensional; eauto. intros y ?. unfold update. destruct eq_dec; eauto; subst; easy. + intros [s' t'] ?; eapply IHunify in H4 as H4'; unfold unifies in *; cbn in *. mapinj; destruct x0 as [u v]; injection H5 as <- <-. rewrite update_irrelevant. symmetry. rewrite update_irrelevant. symmetry. now rewrite H4'. all: intros ? % singlepoint_subst_vars_variable; easy. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)