proposition: Theorem wf_trans_clos : well_founded R -> well_founded trans_clos.
proof: Proof. unfold well_founded; auto with Relations. Defined.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics