#f1 #I1 #I * -I1 -I #I1 [2: #V1 #V #HV1 ] #f2 #I2 #H
[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H
/3 width=6 by lifts_trans, ext2_pair, ext2_unit/
qed-.
#f1 #I1 #I * -I1 -I #I1 [2: #V1 #V #HV1 ] #f2 #I2 #H
[ elim (liftsb_inv_pair_sn … H) | lapply (liftsb_inv_unit_sn … H) ] -H
/3 width=6 by lifts_trans, ext2_pair, ext2_unit/
qed-.