proposition: Lemma unify_lambda_free E sigma: E ↦ sigma -> all_terms (@lambda_free X) E -> forall x, lambda_free (sigma x).
proof: Proof. induction 1. - intros; eauto using @lambda_free. - intros H'; eapply decomp'_lambda_free in H; eauto. simplify in H. intros y; unfold update; destruct eq_dec; subst;intuition idtac. eapply lambda_free_substitution; eauto; intros x; intros. all: eapply IHunify; eapply lambda_free_subst_eqs; eauto. all: intros z; unfold update; destruct eq_dec; intuition econstructor. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)