/3 width=14 by gcp2_lifts_all, gcp2_lifts, gcp0_lifts, lifts_simple_dx, conj/
| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
/3 width=14 by gcp2_lifts_all, gcp2_lifts, gcp0_lifts, lifts_simple_dx, conj/
| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct