proposition: Theorem wf_trans_clos : well_founded R -> well_founded trans_clos.
proof: Proof. unfold well_founded; 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