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