-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