proposition: Lemma inhab_app Gamma Delta x A: Gamma ⊢(1) inhab x A : A -> Delta ++ Gamma ⊢(1) inhab (length Delta + x) A : A.
proof: Proof. intros H % inhab_typing_inv. eapply inhab_typing. rewrite nth_error_app2; simplify; eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)