proposition: Lemma unify_free' E sigma: E ↦ sigma -> free' sigma.
proof: Proof. induction 1. - split; intuition trivial. now destruct H1 as [[= ->]|[]]. - destruct IHunify; split; intros y; intros. + unfold update, bound in *; destruct eq_dec; subst; intuition auto. + unfold update in H7; destruct eq_dec; subst; eauto. eapply vars_subst in H7 as [y']. destruct H7; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)