proposition: Lemma clos_trans_transp_permute : forall x y, transp _ (clos_trans R) x y <-> clos_trans (transp _ R) x y.
proof: Proof. split; induction 1; (apply t_step; assumption) || eapply t_trans; eassumption. Qed.
imports: Relation_Definitions Relation_Operators