| #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
| #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct