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