proposition: Lemma unification_downcast sigma Gamma s t Delta A: Delta ⊩ sigma : Gamma -> Gamma ⊢(n) s : A -> Gamma ⊢(n) t : A -> sigma • s ≡ sigma • t -> exists Sigma tau, Sigma ⊩(n) tau : Gamma /\ tau • s ≡ tau • t.
proof: Proof. Proof using Leq. intros T T1 T2 H. pose (P x := x ∈ vars s ++ vars t). edestruct (downcast_variables) as (Sigma' & tau' & T' & H' & O'); [eassumption..|]; clear T H sigma Delta. edestruct (downcast_constants) as (Sigma'' & tau'' & T'' & H'' & O'' & C''); [eassumption..|]; clear T' H' tau'. edestruct (normalise_subst) as (tau''' & R & H & T); [eassumption|]. eapply ordertyping_weak_ordertyping with (sigma := tau'''). - intros. eapply ordertyping_from_basetyping. + intros ?; erewrite consts_subset_steps; trivial. intros H2 % C''; cbn in H2; simplify in H2. destruct H2; eapply typing_constants; [|eauto| |eauto]; eauto. + eauto. + domin H0; eauto. + simplify in H1; destruct H1; eapply vars_ordertyping_nth; eauto. + simplify; rewrite O', O''; cbn; eauto. - rewrite !subst_pointwise_equiv with (sigma := tau''') (tau := tau''); eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)