proposition: Lemma ren_step s t delta: s > t -> ren delta s > ren delta t.
proof: Proof. induction 1 in delta |-*; cbn; eauto. econstructor. subst. now asimpl. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun