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. split. - apply (trans_clos_t1n x y). - apply (clos_t1n_trans x y). Defined.
imports: Equations.Init Equations.HoTT.Logic Equations.HoTT.Relation