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