proposition: Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans_n1 R y x.
proof: Proof. intros x y H; elim H. - constructor 1. - intros y0 z D H0 H1. apply clos_rstn1_trans with y0; auto. right with z. + destruct D; auto with relations. + left. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation