-lemma cnx_appl_simple: ∀h,o,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → 𝐒⦃T⦄ →
- ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓐV.T⦄.
-#h #o #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H //
+lemma cnx_appl_simple (G) (L):
+ ∀V,T. ❪G,L❫ ⊢ ⬈𝐍 V → ❪G,L❫ ⊢ ⬈𝐍 T → 𝐒❪T❫ → ❪G,L❫ ⊢ ⬈𝐍 ⓐV.T.
+#G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H //