- lapply (IH1 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #HV2
- lapply (IH1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ #HT2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_fpbg/ #H2l0
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fsupp_fpbg/ -HV1 #W2 #HVW2 #HW12
- elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fsupp_fpbg/ -HT12 -HTU1 #X #HTU2 #H
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+ lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0
+ elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12
+ elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H