proposition: Lemma unifies_free_all sigma x s: ~ x ∈ vars s -> free' sigma -> free x -> unifies sigma (var x) s -> (forall y, y ∈ vars s -> free y) .
proof: Proof. Proof using isFree. intros H1 F H2 H3 y H4; unfold unifies in *; cbn in *. destruct F as [F1 F2]. destruct (isFree y) as [H|H]; eauto. specialize (F2 _ H2) as H5. rewrite H3 in H5. eapply H5. eapply subst_vars. eauto. rewrite F1. cbn; eauto. now unfold bound. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)