theorem nta_abst_repellent (a) (h) (p) (G) (K):
∀W,T,U1. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[a,h] U1 →
∀U2. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U2 → ⬆*[1] U1 ≘ U2 → ⊥.
theorem nta_abst_repellent (a) (h) (p) (G) (K):
∀W,T,U1. ⦃G,K⦄ ⊢ ⓛ{p}W.T :[a,h] U1 →
∀U2. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U2 → ⬆*[1] U1 ≘ U2 → ⊥.