proposition: Lemma unify_complete sigma E: free' sigma -> Unifies sigma E -> all_terms (@lambda_free X) E -> exists tau, E ↦ tau.
proof: Proof. Proof using isFree. intros F; induction E as [E IH] using eqs_size_induction; intros U LF. destruct (decomp' E) as [[| [t s] E']|] eqn: DE. - exists var. now econstructor. - eapply decomp'_some_var in DE as H'; cbn in H'; destruct H' as [x ->]. eapply equi_unifiable_decomp' in DE as U'. eapply U' in U as H4; simplify in H4; destruct H4 as [H4 H5]; cbn in H4. eapply unifies_not_var in H4 as H6; [| eapply decomp'_irrefl; eauto; firstorder]. eapply unifies_free in H6 as H7; eauto. specialize (unifies_free_all H6 F H7 H4) as H8. eapply Vars_decomp' in DE as H9; simplify in H9; cbn in H9. assert (Vars' (update x s var •₊₊ E') ⊆ Vars' E) by (rewrite singlepoint_subst_Vars'; eapply incl_cons_project_r; eauto). destruct (IH (update x s var •₊₊ E') x) as [tau]; trivial. + eapply H9; firstorder. + intros ? % singlepoint_subst_Vars'_variable; easy. + rewrite equi_unifiable_cons in U'. eapply U' in U; simplify in U; easy. + eapply decomp'_lambda_free in DE; eauto; simplify in DE; eauto. eapply lambda_free_subst_eqs; intuition idtac; eauto. unfold update; destruct eq_dec; (intuition auto); eauto using lambda_free. + exists (update x (tau • s) tau); econstructor; eauto. - eapply decomp'_none_not_unifiable in DE; intuition eauto. exfalso; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)