proposition: Lemma clos_rtn1_step : forall x y, R x y -> clos_refl_trans_n1 R x y.
proof: Proof. intros x y H. right with x;[assumption|left]. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation