proposition: Theorem Rstar_equiv_Rstar1 : forall (U:Type) (R:Relation U), same_relation U (Rstar U R) (Rstar1 U R).
proof: Proof. generalize Rstar_contains_R; intro T; red in T. intros U R; unfold same_relation, contains. split; intros x y H'; elim H'; auto with sets. - generalize Rstar_transitive; intro T1; red in T1. intros x0 y0 z H'0 H'1 H'2 H'3; apply T1 with y0; auto with sets. - intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto with sets. Qed.
imports: Relations_1 Relations_1_facts Relations_2