#h #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
@(IH (ⓑ{p, I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2
#h #G #L #U #H elim H -H #U0 #_ #IH #p #I #V #T #H destruct
@csx_intro #T2 #HLT2 #HT2
@(IH (ⓑ{p, I}V.T2)) -IH /2 width=3 by cpx_bind/ -HLT2