proposition: Lemma vars_decomp s t E: decomp s t = Some E -> Vars' E ⊆ vars s ++ vars t.
proof: Proof. decomp_ind; cbn; intros; simplify. 1-2:easy. now intros ? [->|];eauto using in_or_app,in_eq. rewrite H1, H3. (repeat eapply incl_app_build); intros ?; simplify. all:tauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)