proposition: Lemma inhab_typing' Gamma x A: nth Gamma x = Some A -> target' Gamma ⊢(1) inhab x A : A.
proof: Proof. intros H; eapply inhab_typing. unfold target'; erewrite map_nth_error; now eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)