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