proposition: Lemma singlepoint_subst_Vars' x s E: Vars' (update x s var •₊₊ E) ⊆ vars s ++ Vars' E.
proof: Proof. induction E as [|[u v]]; [cbn; easy|]; simplify. cbn; rewrite !singlepoint_subst_vars, IHE, <-!app_assoc. repeat eapply incl_app_build. all:eauto using incl_refl,incl_appr,incl_appl. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)