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