proposition: Lemma trans_clos_transp_permute : forall x y, transp (trans_clos R) x y <-> trans_clos (transp R) x y.
proof: Proof. split; induction 1; (apply t_step; assumption) || eapply t_trans; eassumption. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation