- [ -HT1 elim (fqup_inv_step_sn … HT2) -HT2
- /4 width=9 by fpbsa_inv_fpbs, fpbc_fqu, ex3_2_intro, ex2_3_intro/
- | elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H
- /5 width=9 by fpbsa_inv_fpbs, fpbc_cpx, fqup_fqus, ex3_2_intro, ex2_3_intro/
+ [ -HT1 /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/
+ | /5 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, fqup_fqus, ex3_2_intro, ex2_3_intro/
+ ]
+| #G2 #L #L0 #L2 #T #T2 #HT1 #HT2 #HL0 #H0 #HL02 #H02
+ lapply (lpxs_trans … HL0 … HL02) #HL2
+ elim (eq_term_dec T1 T) #H destruct
+ [ -HT1 elim (fqus_inv_gen … HT2) -HT2
+ [ /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/
+ | * #H1 #H2 #H3 destruct
+ /4 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro/
+ ]
+ | /4 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, ex3_2_intro, ex2_3_intro/