proposition: Lemma normal_subst s sigma: (forall x, ~ isLam (sigma x)) -> (forall x, normal (sigma x)) -> normal s -> normal (sigma • s).
proof: Proof. induction s in sigma |-*; intros H1 H2 N; cbn in *; intuition. - eapply normal_lam_intro, IHs; [| | now eapply normal_lam_elim]. + intros []; cbn; intuition. unfold funcomp in *. eapply H1 with (x := n). destruct sigma; cbn; intuition. + intros []; cbn; intuition. now eapply normal_ren. - eapply normal_app_intro; eauto. destruct s1; eauto. intros _; eapply N; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun