lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20