proposition: Lemma incl_trans_clos : inclusion R trans_clos.
proof: Proof. red; auto with relations. Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties