proposition: Theorem Rstar_contains_Rplus : forall (U : Type) (R : Relation U), Contains (Rstar R) (Rplus R).
proof: Proof. intros U R; red in |- *. intros x y H'; elim H'. generalize Rstar_contains_R; intro T; red in T; auto. intros x0 y0 z H'0 H'1 H'2; apply Rstar_n with y0; auto. Qed.
imports: Relations Confluence