proposition: Theorem Rstar_cases : forall (U : Type) (R : Relation U) (x y : U), Rstar R x y -> x = y \/ (exists u : U, R x u /\ Rstar R u y).
proof: Proof. intros U R x y H'; elim H'; auto. intros x0 y0 z H'0 H'1 H'2; right; exists y0; auto. Qed.
imports: Relations Confluence