proposition: Theorem Rstar_contains_R : forall (U:Type) (R:Relation U), contains U (Rstar U R) R.
proof: Proof. intros U R; red; intros x y H'; apply Rstar_n with y; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2