proposition: Lemma clos_rt_rt1n : forall x y, clos_refl_trans R x y -> clos_refl_trans_1n R x y.
proof: Proof. induction 1. - apply clos_rt1n_step; assumption. - left. - generalize IHX2; clear IHX2; induction IHX1; auto. right with y; auto. eapply IHIHX1; auto. apply clos_rt1n_rt; auto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation