proposition: Lemma lambda_free_subst Delta (sigma: fin -> exp X) x A: (Delta ⊢(1) sigma x : A) -> ord A <= 1 -> normal (sigma x) -> lambda_free (sigma x).
proof: Proof. intros H1 H3 H4; eapply order_one_lambda_free; [eauto..|]. eapply head_atom; eauto. destruct sigma; cbn; intuition idtac. inv H1. eapply ord_arr_one; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)