| #p #I #V1 #T1 #_ #IH #H
elim (cnv_inv_bind … H) -H #HV1 #HT1
elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12
| #p #I #V1 #T1 #_ #IH #H
elim (cnv_inv_bind … H) -H #HV1 #HT1
elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12