-lemma cnx_appl_simple: ∀h,g,L,V,T. ⦃h, L⦄ ⊢ 𝐍[g]⦃V⦄ → ⦃h, L⦄ ⊢ 𝐍[g]⦃T⦄ → 𝐒⦃T⦄ →
- ⦃h, L⦄ ⊢ 𝐍[g]⦃ⓐV.T⦄.
-#h #g #L #V #T #HV #HT #HS #X #H
-elim (cpx_inv_appl1_simple … H ?) -H // #V0 #T0 #HV0 #HT0 #H destruct
+lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → 𝐒⦃T⦄ →
+ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄.
+#h #g #G #L #V #T #HV #HT #HS #X #H
+elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct