proposition: Theorem Rstar_equiv_Rstar1 : forall (U : Type) (R : Relation U), Same_relation (Rstar R) (Rstar1 R).
proof: Proof. generalize Rstar_contains_R; intro T; red in T. intros U R; unfold Same_relation, Contains in |- *. split; intros x y H'; elim H'; auto. 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. intros x0 y0 z H'0 H'1 H'2; apply Rstar1_n with y0; auto. Qed.
imports: Relations Confluence