proposition: Lemma equi_unifiable_cons x s E: (var x, s) :: E ≈ (var x, s) :: (update x s var •₊₊ E).
proof: Proof. intros ?; simplify; intuition idtac; cbn in *. - intros [u v] ?; mapinj; cbn; destruct x0 as [u' v']. injection H2 as <- <-. eapply H1 in H3; cbn in H3. unfold unifies in *; cbn in *. asimpl. etransitivity; [ etransitivity; [| eapply H3] |]. all: eapply ext_exp; intros y; unfold funcomp, update; destruct eq_dec; subst; eauto. - intros [u v] ?; cbn. unfold unifies in H0; cbn in H0. eapply in_map with (f := subst_eq (update x s var)) in H. eapply H1 in H; cbn in H; unfold unifies in H. unfold unifies in *; cbn in *. asimpl in H. etransitivity; [ etransitivity; [| eapply H] |]. all: eapply ext_exp; intros y; unfold funcomp, update; destruct eq_dec; subst; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)