proposition: Lemma lambda_free_AppR s T: lambda_free s -> (forall t, t ∈ T -> lambda_free t) -> lambda_free (AppR s T).
proof: Proof. induction T; cbn; intuition (econstructor; eauto). Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)