- /3 width=1 by fpb_fqu, fdeq_intro_sn, or_intror, or_introl/
-| #T2 #H elim (tdeq_dec T1 T2)
- /4 width=1 by fpb_cpx, fdeq_intro_sn, or_intror, or_introl/
-| #L2 elim (rdeq_dec L1 L2 T1)
- /4 width=1 by fpb_lpx, fdeq_intro_sn, or_intror, or_introl/
+ /3 width=1 by fpb_fqu, feqx_intro_sn, or_intror, or_introl/
+| #T2 #H elim (teqx_dec T1 T2)
+ /4 width=1 by fpb_cpx, feqx_intro_sn, or_intror, or_introl/
+| #L2 elim (reqx_dec L1 L2 T1)
+ /4 width=1 by fpb_lpx, feqx_intro_sn, or_intror, or_introl/