proposition: Lemma clos_rt_rtn1 : forall x y, clos_refl_trans R x y -> clos_refl_trans_n1 R x y.
proof: Proof. induction 1. - apply clos_rtn1_step; auto. - left. - elim IHX2; auto. intros. right with y0; auto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation