proposition: Lemma clos_r_clos_rt : inclusion (clos_refl R) (clos_refl_trans R).
proof: Proof. induction 1 as [? ?| ]. - constructor; auto. - constructor 2. Defined.
imports: CRelationClasses Equations.Init Equations.Type.Logic Equations.Type.Relation