proposition: Lemma unification_downcast_eqs sigma Delta (E: eqs X) Gamma L: (Gamma ⊢₊₊(n) E : L) -> (Delta ⊩ sigma : Gamma) -> (sigma •₊ left_side E) ≡₊ (sigma •₊ right_side E) -> exists Sigma tau, Sigma ⊩(n) tau : Gamma /\ (tau •₊ left_side E) ≡₊ (tau •₊ right_side E).
proof: Proof. Proof using Leq. intros T1 T2 H. pose (P x := x ∈ Vars' E). pose (s := linearize_terms (left_side E)). pose (t := linearize_terms (right_side E)). edestruct (downcast_variables) with (s := s) (t := t) as (Sigma' & tau' & T' & H' & O'); [eassumption|..]. 1: unfold s, t; now rewrite !linearize_terms_subst, linearize_terms_equiv. clear T2 H sigma Delta. edestruct (downcast_constants) with (s := s) (t := t) as (Sigma'' & tau'' & T'' & H'' & O'' & C''); eauto; clear T' H' tau'. edestruct (normalise_subst) as (tau''' & R & H & T); eauto. edestruct ordertyping_weak_ordertyping with (s := s) (t := t) (sigma := tau'''). - intros. eapply ordertyping_from_basetyping. + intros ?; erewrite consts_subset_steps; trivial. intros H2 % C''. cbn [Consts flat_map] in H2. simplify in H2. unfold s, t in H2. rewrite !linearize_consts in H2. destruct H2; eapply typing_Consts. eapply left_ordertyping; [eassumption|..]. eauto. eapply right_ordertyping; eauto. eauto. + eauto. + domin H0; eauto. + simplify in H1. unfold s, t in H1; rewrite !linearize_vars in H1. destruct H1 as [H1|H1]; eapply Vars_listordertyping in H1. 2, 4: eauto using left_ordertyping, right_ordertyping. all: destruct H1 as [? [H1 H2]]; rewrite H0 in H1; injection H1 as ->; eauto. + simplify; rewrite O', O''; cbn; eauto. - rewrite !subst_pointwise_equiv with (sigma := tau''') (tau := tau''); eauto. - destruct H0 as [tau]. exists x. exists tau. destruct H0; split; trivial. unfold s, t in H1; now rewrite <-linearize_terms_equiv, <-!linearize_terms_subst. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)