proposition: Lemma ren_equiv s t delta: s ≡ t -> ren delta s ≡ ren delta t.
proof: Proof. intros (v & ? & ?) % church_rosser; trivial. transitivity (ren delta v); [| symmetry]. all: eapply equiv_star, ren_steps; eauto. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)