proposition: Lemma equiv_lam_elim (s t: exp X): lambda s ≡ lambda t -> s ≡ t.
proof: Proof. intros (v & [] %steps_lam & [] %steps_lam) % church_rosser; [|eauto]. intuition idtac; subst. injection H as ->; eauto. Qed.
imports: Morphisms Lia FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics confluence)