#V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (โV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (โV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
#V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (โV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (โV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //