- lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fsupp_fpbg, cpr_lpr_fpbs/ #HW4
- lapply (IH3 … HW23 … HL12) /2 width=1 by fsupp_fpbg/ #HW3
- lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fsupp_fpbg/ #HW3l
- elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fsupp_fpbg, lpr_pair/ #U3 #HTU3 #HU23
+ lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
+ lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3
+ lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3l
+ elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23