- lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3 by ldrops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip/
+ lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by ldrops_trans, lifts_trans/ #HLW2B
+ @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
+ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip, lifts_trans/