proposition: Lemma clos_rtn1_rt : forall x y, clos_refl_trans_n1 R x y -> clos_refl_trans R x y.
proof: Proof. induction 1. - constructor 2. - constructor 3 with y; auto. constructor 1; assumption. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation