elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
@(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
@(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/