proposition: Lemma trans_clos_t1n_iff : forall x y, trans_clos R x y <-> trans_clos_1n R x y.
proof: Proof. intros x y. exists (trans_clos_t1n x y). apply (clos_t1n_trans x y). Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation