proposition: Lemma unifies_not_var x s tau: var x <> s -> unifies tau (var x) s -> ~ x ∈ vars s.
proof: Proof. intros H1; unfold unifies; cbn; intros S % (f_equal size). rewrite size_subst in S. intros H; eapply H1; eapply in_map with (f := tau >> size) in H as H'. eapply Sum_in in H'. eapply vars_varof in H; inv H; cbn in *; eauto. all: unfold funcomp in *; lia. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)