| lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
]
| lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
]
elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
| #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
elim (lift_total V 0 (i+1)) /3 width=10/
| #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
elim (lift_total V 0 (i+1)) /3 width=10/