proposition: Lemma trans_clos_tn1_iff : forall x y, trans_clos R x y <-> trans_clos_n1 R x y.
proof: Proof. split. - apply trans_clos_tn1. - apply clos_tn1_trans. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation