proposition: Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R).
proof: Proof. apply Build_equivalence. - exact (rst_refl A R). - exact (rst_trans A R). - exact (rst_sym A R). Qed.
imports: Relation_Definitions Relation_Operators