proposition: Lemma lambda_free_subst_eqs sigma E: (forall x, x ∈ Vars' E -> lambda_free (sigma x)) -> all_terms lambda_free E -> all_terms lambda_free (sigma •₊₊ E).
proof: Proof. intros H; induction E as [| [s t]]; cbn; eauto; simplify; cbn in *. intros (H1 & H2 & H3). split; [|split]. 1 - 2: eapply lambda_free_substitution; eauto; intros; eapply H; intuition (auto with datatypes). eapply IHE; eauto; intuition (auto with datatypes); now eapply H. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)