- lapply (IH … HA … (L2.ⓓV2) … HT10) -IH -HA -HT10 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
- | -B #T #HT1 #HTX
- elim (lift_total X 0 1) #X1 #HX1
- lapply (tpr_lift … HTX … HT1 … HX1) -T #HTX1
- lapply (IH … HA … (L2.ⓓV1) … HTX1) /width=5/ -T1 /2 width=1/ -L1 #HA
- @(aaa_inv_lift … HA … HX1) /2 width=1/
+ lapply (IH … HA … (L2.ⓓV2) … HT1) -IH -HA -HT1 /width=5/ -T1 /2 width=1/ -L1 -V1 /3 width=5/
+ | -B #T #HT1 #HXT #H destruct
+ lapply (IH … HA … (L2.ⓓV1) … HT1) /width=5/ -T1 /2 width=1/ -L1 #HA
+ @(aaa_inv_lift … HA … HXT) /2 width=1/