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
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