proposition: Lemma unif (E: list (exp X * exp X)) : { sigma | E ↦ sigma } + ({ sigma | E ↦ sigma } -> False).
proof: Proof. Proof using isFree. pattern E. revert E. apply (well_founded_induction_type wf_subvars). intros E unif. destruct (decomp' E) as [[|[[x| | |] s] E']|] eqn:H. 1: left; exists var; now econstructor. 2-5: right; intros [σ H']; inv H'; congruence. destruct (x el vars s) as [?|?]. { right; intros [σ H']; inv H'; congruence. } destruct (isFree x) as [?|?]. 2: { right; intros [σ H']; inv H'; congruence. } destruct (dec_all isFree (vars s)) as [?|?]. 2: { right. intros [σ H']; inv H'; [congruence|]. rewrite H in H0. inv H0; eauto. } destruct (unif [subst_eq (update x s var) p | p ∈ E']) as [[sigma IH]|IH]. { unfold subvars, MR. eapply Vars_decomp' in H. split. + rewrite singlepoint_subst_Vars'. cbn in H. lauto. + exists x. split. cbn in H; lauto. intros ? % singlepoint_subst_Vars'_variable. easy. } - left. exists (update x (sigma • s) sigma). econstructor; eauto. - right; intros [σ H']; inv H'; [congruence|]. rewrite H in H0. inv H0. eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)