proposition: Lemma WellFounded_trans_clos `(WF : WellFounded A R) : WellFounded (trans_clos R).
proof: Proof. apply wf_trans_clos. apply WF. Defined.
imports: Equations(Init Signature) Equations.CoreTactics Equations.Type.Logic Equations.Type.Classes Equations.Type.EqDec Equations.Type.Relation Equations.Type.FunctionalExtensionality Equations.Type.WellFounded Equations.Type.DepElim Equations.Type.Constants