-lemma cnx_inv_abst: ∀h,p,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓛ[p]V.T❫ →
- ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ ∧ ❪G,L.ⓛV❫ ⊢ ⬈[h] 𝐍❪T❫.
-#h #p #G #L #V1 #T1 #HVT1 @conj
+lemma cnx_inv_abst (G) (L):
+ ∀p,V,T. ❨G,L❩ ⊢ ⬈𝐍 ⓛ[p]V.T →
+ ∧∧ ❨G,L❩ ⊢ ⬈𝐍 V & ❨G,L.ⓛV❩ ⊢ ⬈𝐍 T.
+#G #L #p #V1 #T1 #HVT1 @conj