proposition: Lemma ren_steps s t delta: s >* t -> ren delta s >* ren delta t.
proof: Proof. induction 1; eauto using ren_step. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun