proposition: Lemma clos_rst_is_equiv : Equivalence (clos_refl_sym_trans R).
proof: Proof. constructor. - exact (rst_refl R). - exact (rst_sym R). - exact (rst_trans R). Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation