∧∧ ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃V⦄ & ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ & 𝐒⦃T⦄.
#h #G #L #V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2
∧∧ ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃V⦄ & ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ & 𝐒⦃T⦄.
#h #G #L #V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2