proposition: Lemma inhab_typing Delta x A: nth Delta x = Some (target A) -> Delta ⊢(1) inhab x A : A.
proof: Proof. intros H2. unfold inhab. destruct (type_decompose A) as (L & beta & ->); simplify in H2; cbn in H2. specialize (arity_decomposed L beta) as H3. rewrite H3. eapply Lambda_ordertyping; trivial. econstructor; cbn; trivial. rewrite nth_error_app2; simplify; trivial; lia. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)