- lapply (lsubsv_fwd_lsubd … HK12) #H
- lapply (lsubd_da_trans … HV0 … H) -H #H
- elim (da_inv_sta … H) -H
- elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y1
+ elim (IHVW … HV0 … HK12) -K2 /3 width=5 by lstas_zero, ex2_intro/
+ | #V1 #l1 #_ #_ #HV1 #HV #HK12 #_ #H destruct
+ lapply (da_mono … HV0 … HV) -HV #H destruct
+ elim (da_lstas … HV1 0) -HV1 #W1 #HVW1 #_
+ elim (lift_total W1 0 (i+1)) #U1 #HWU1
+ elim (IHVW … HV0 … HK12) -K2 // #X #HVX #_ -W
+ @(ex2_intro … U1) /3 width=6 by lstas_cast, lstas_ldef/ (**) (* full auto too slow *)
+ @cpcs_cprs_sn @(cprs_delta … HLK1 … HWU1)
+ /4 width=2 by cprs_strap1, cpr_cprs, lstas_cpr, cpr_eps/
+ ]
+| #G #L2 #K2 #V #W #U #i #l2 #HLK2 #_ #HWU #IHVW #l1 #Hl21 #Hl1 #L1 #HL12
+ elim (da_inv_lref … Hl1) -Hl1 * #K0 #V0 [| #l0 ] #HK0 #HV0 [| #H1 ]
+ lapply (drop_mono … HK0 … HLK2) -HK0 #H2 destruct
+ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21
+ elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #Y #H #HLK1
+ elim (lsubsv_inv_pair2 … H) -H * #K1
+ [ #HK12 #H destruct
+ elim (IHVW … Hl21 HV0 … HK12) -K2 -Hl21 #X