proposition: Fact normal_form_ren' xi M : normal_form (ren xi M) -> normal_form M.
proof: Proof. elim: M xi=> /=. - by eauto using normal_form. - move=> [?|??|?] /= IH1 ? IH2 ? /normal_formE. + by eauto using normal_form. + move=> [??]. by eauto using normal_form. + done. - move=> ??? /normal_formE. by eauto using normal_form. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect