elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct
lapply (lift_inj … HY … HW01) -HY #H destruct
/3 width=6 by snv_appl/
| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0
elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct
lapply (lift_inj … HY … HW01) -HY #H destruct
/3 width=6 by snv_appl/
| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H
elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct
elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0