proposition: Theorem star_monotone : forall (U : Type) (R S : Relation U), Contains S R -> Contains (Rstar S) (Rstar R).
proof: Proof. intros U R S H'. apply Sstar_contains_Rstar. generalize (Rstar_contains_R (R:=S)); auto. Qed.
imports: Relations Confluence