proposition: Lemma normal_ren s delta: normal s -> normal (ren delta s).
proof: Proof. induction s in delta |-*; cbn; intuition. eapply normal_app_intro; eauto. destruct s1; cbn; eauto. intros _; eapply H; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun