proposition: Lemma inhab_typing_inv Gamma x A: Gamma ⊢(1) inhab x A : A -> nth Gamma x = Some (target A).
proof: Proof. intros H; unfold inhab in H. eapply Lambda_ordertyping_inv in H as (L & B & ? & ? & ?); subst. inv H. rewrite <-H1 in H3. rewrite nth_error_app2 in H3; simplify in *; trivial. destruct B; cbn in H1; try lia. now rewrite H3. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)