-lemma cnx_inv_appl: ∀h,G,L,V,T. ❪G,L❫ ⊢ ⬈[h] 𝐍❪ⓐV.T❫ →
- ∧∧ ❪G,L❫ ⊢ ⬈[h] 𝐍❪V❫ & ❪G,L❫ ⊢ ⬈[h] 𝐍❪T❫ & 𝐒❪T❫.
-#h #G #L #V1 #T1 #HVT1 @and3_intro
+lemma cnx_inv_appl (G) (L):
+ ∀V,T. ❪G,L❫ ⊢ ⬈𝐍 ⓐV.T →
+ ∧∧ ❪G,L❫ ⊢ ⬈𝐍 V & ❪G,L❫ ⊢ ⬈𝐍 T & 𝐒❪T❫.
+#G #L #V1 #T1 #HVT1 @and3_intro