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