proposition: Lemma eqs_size_induction P: (forall E, (forall E' x, Vars' E' ⊆ Vars' E -> x ∈ Vars' E -> ~ x ∈ Vars' E' -> P E') -> P E) -> forall E, P E.
proof: Proof. intros IH E. eapply well_founded_induction_type. eapply measure_wf, wf_strict_incl with (X := nat); typeclasses eauto. intros x H; eapply IH; intros; eapply H. split; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)