proposition: Theorem star_monotone : forall (U:Type) (R S:Relation U), contains U S R -> contains U (Rstar U S) (Rstar U R).
proof: Proof. intros U R S H'. apply Sstar_contains_Rstar; auto with sets. generalize (Rstar_contains_R U S); auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2