proposition: Lemma confluence_unique_normal_forms R x y z: confluent R -> Normal R y -> Normal R z -> star R x y -> star R x z -> y = z.
proof: Proof. intros H1 H2 H3 H4 H5. destruct (H1 _ _ _ H4 H5) as [x' A B]. destruct A; [destruct B | ]; eauto; exfalso; [ eapply H3 | eapply H2 ]; eauto. Qed.
imports: Morphisms FinFun Undecidability.HOU(std.tactics std.misc std.ars.basic)