-| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0
- [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (fquq_cpxs_trans … HT03 … H10) -T0
- /3 width=9 by fqus_strap2, ex4_5_intro/
- | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- /3 width=9 by cpxs_strap2, ex4_5_intro/
- | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42
- lapply (lpx_cpxs_trans … HT13 … HL10) -HT13 #HT13
- elim (lpx_fqus_trans … H34 … HL10) -L0
- /3 width=9 by lpxs_step_sn, cpxs_trans, ex4_5_intro/
- | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (feqg_cpxs_trans … H10 … HT03) -T0 // #T0 #HT10 #H03
- elim (feqg_fqus_trans … H03 … H34) -G0 -L0 -T3 // #G0 #L0 #T3 #H03 #H34
- elim (feqg_lpxs_trans … H34 … HL34) -L3 // #L3 #HL03 #H34
- /3 width=13 by feqg_trans, ex4_5_intro/
- ]
+| #G1 #G0 #L1 #L0 #T1 #T0 *
+ #L3 #T3 #H13 #HT30 #HL30 #_ *
+ #G4 #L4 #L5 #T4 #T5 #HT04 #H45 #HL45 #H52
+ lapply (rpx_cpx_conf_sn … HT30 … HL30) -HL30 #HL30
+ elim (fquq_cpx_trans … H13 … HT30) -T3 #T3 #HT13 #H30
+ elim (rpx_fwd_lpx_reqg S … HL30) -HL30 // #L #HL3 #HL0
+ lapply (reqg_cpxs_trans … HT04 … HL0) -HT04 // #HT04
+ lapply (cpxs_reqg_conf_sn … HT04 … HL0) -HL0 #HL0
+ lapply (lpx_cpxs_trans … HT04 … HL3) -HT04 #HT04
+ elim (fquq_cpxs_trans … HT04 … H30) -T0 #T0 #HT30 #H04
+ lapply (cpxs_strap2 … HT13 … HT30) -T3 #HT10
+ elim (reqg_fqus_trans … H45 … HL0) -L0 // #L0 #T3 #H43 #HT35 #HL04
+ lapply (feqg_intro_dx … G4 … HL04 … HT35) -HL04 -HT35 // #H35
+ elim (lpx_fqus_trans … H43 … HL3) -L #L #T #HT4 #H3 #HL0
+ elim (fquq_cpxs_trans … HT4 … H04) -T4 #T4 #HT04 #H4
+ lapply (cpxs_trans … HT10 … HT04) -T0 #HT14
+ lapply (fqus_strap2 … H4 … H3) -G0 -L3 -T #H43
+ elim (feqg_lpxs_trans … H35 … HL45) -L4 // #L4 #HL04 #H35
+ lapply (lpxs_step_sn … HL0 … HL04) -L0 #HL4
+ lapply (feqg_trans … H35 … H52) -L5 -T5 // #H32
+ /2 width=9 by ex4_5_intro/