proposition: Lemma lambda_free_substitution sigma s: lambda_free s -> (forall x, x ∈ vars s -> lambda_free (sigma x)) -> lambda_free (sigma • s).
proof: Proof. induction 1; cbn; eauto using lambda_free. intros; econstructor; eauto; [eapply IHlambda_free1 | eapply IHlambda_free2]; intuition (auto with datatypes). Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)