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