[ elim (fquq_cpxs_trans … HT0 … HG1) -T
/3 width=7 by fqus_strap2, ex3_2_intro/
| /3 width=5 by cpxs_strap2, ex3_2_intro/
-| lapply (cpxs_llpx_trans … HT0 … HL1) -HT0 #HT10
+| lapply (llpx_cpxs_trans … HT0 … HL1) -HT0 #HT10
lapply (cpxs_llpx_conf … HT10 … HL1) -HL1 #HL1
elim (llpx_fqus_trans … HG2 … HL1) -L
/3 width=7 by llpxs_strap2, cpxs_trans, ex3_2_intro/