proposition: Lemma Vars_decomp' E E': decomp' E = Some E' -> Vars' E' ⊆ Vars' E.
proof: Proof. decomp_ind. easy. intros. simplify. now rewrite H1, vars_decomp; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)