proposition: Lemma unifies_free sigma x s: ~ x ∈ vars s -> free' sigma -> unifies sigma (var x) s -> free x.
proof: Proof. Proof using isFree. intros H1 F H2; unfold unifies in *; cbn in *. destruct F as [F1 F2]. destruct (isFree x) as [H|H]; eauto. eapply F1 in H as H'. rewrite H' in H2. destruct s; try discriminate; cbn in H2. destruct (isFree f) as [L|L]; eauto. - eapply F2 with (y := x) in L; eauto; rewrite <-H2; cbn; auto. - exfalso; eapply H1; left; eapply F1 in L; congruence. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)