proposition: Lemma ordertyping_weak_ordertyping Gamma Delta sigma (s t: exp X): (forall x A, nth Gamma x = Some A -> x ∈ vars s ++ vars t -> Delta ⊢(n) sigma x : A) -> sigma • s ≡ sigma • t -> (exists Sigma tau, Sigma ⊩(n) tau : Gamma /\ tau • s ≡ tau • t).
proof: Proof. Proof using Leq. intros T EQ. pose (tau x := if x el (vars s ++ vars t) then sigma x else match nth Gamma x with | Some A => inhab X (length Delta + x) A | None => var x end). exists (Delta ++ target' Gamma). exists tau. split. - intros x B H'. unfold tau. rewrite H'; destruct dec_in. eapply weakening_ordertyping_app, T; trivial. eapply ordertyping_monotone; eauto. - rewrite !(subst_extensional) with (sigma := tau) (tau := sigma); trivial. all: intros; unfold tau; destruct dec_in; trivial; simplify in *. all: exfalso; eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)