proposition: Lemma trans_clos_tn1 : forall x y, trans_clos R x y -> trans_clos_n1 R x y.
proof: Proof. induction 1. - left; assumption. - elim IHX2. -- intro y0; right with y; auto. -- intros. right with y0; auto. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation