- /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/
-| /2 width=1 by or_introl/
+ [ #H elim H -H /2 width=1 by feqg_refl/
+ | /2 width=1 by fpb_fqu/
+ ]
+| /4 width=1 by fpb_cpx, teqg_feqg/
+| /4 width=1 by fpb_lpx, feqg_intro_sn/
+| #G2 #L2 #T2 #H12 #Hn12
+ elim Hn12 -Hn12 //