proposition: Theorem Rsym_imp_Rstarsym : forall (U : Type) (R : Relation U), Symmetric R -> Symmetric (Rstar R).
proof: Proof. intros U R H'; red in |- *. intros x y H'0; elim H'0; auto. intros x0 y0 z H'1 H'2 H'3. generalize Rstar_transitive; intro T; red in T. apply T with y0; auto. apply Rstar_n with x0; auto. Qed.
imports: Relations Confluence