proposition: Lemma singlepoint_subst_Vars'_variable x s E: x ∈ Vars' (update x s var •₊₊ E) -> x ∈ vars s /\ x ∈ Vars' E.
proof: Proof. induction E as [|[u v]]; [easy|]; simplify. cbn; simplify; intros [[H % singlepoint_subst_vars_variable | H % singlepoint_subst_vars_variable] | H]. 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)