proposition: Lemma Vars'_app E1 E2: Vars' (E1 ++ E2) = Vars' E1 ++ Vars' E2.
proof: Proof. unfold Vars'; now rewrite !flat_map_app. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)