proposition: Lemma wf_subvars : well_founded subvars.
proof: Proof. eapply measure_wf, wf_strict_incl, eq_dec. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)