proposition: Lemma equiv_anti_ren delta (s t: exp X): Injective delta -> ren delta s ≡ ren delta t -> s ≡ t.
proof: Proof. intros ? (v & H1 & H2) % church_rosser; trivial. eapply steps_anti_ren in H1 as []. eapply steps_anti_ren in H2 as []. intuition idtac; subst. eapply anti_ren in H4; trivial. subst; eauto. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)