proposition: Lemma equiv_unique_normal_forms R x y: confluent R -> equiv R x y -> Normal R x -> Normal R y -> x = y.
proof: Proof. intros ? [v [H1 H2]] % church_rosser ? ?; eauto. inv H1; inv H2; intuition. all: exfalso; firstorder. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)