proposition: Fact normal_form_ren xi M : normal_form M -> normal_form (ren xi M).
proof: Proof. move=> H. elim: H xi; cbn; by eauto using normal_form. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect