-(* Basic_2A1: fpbq_inv_fpb_alt *)
-lemma fpbq_ffdneq_inv_fpb: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1,L1,T1⦄ ≽[h] ⦃G2,L2,T2⦄ →
- (⦃G1,L1,T1⦄ ≛ ⦃G2,L2,T2⦄ → ⊥) → ⦃G1,L1,T1⦄ ≻[h] ⦃G2,L2,T2⦄.
-#h #G1 #G2 #L1 #L2 #T1 #T2 #H #H0
-elim (fpbq_inv_fpb … H) -H // #H elim H0 -H0 //
+(* Basic_2A1: uses: fpbq_ind_alt *)
+lemma fpbq_inv_fpb:
+ ∀G1,G2,L1,L2,T1,T2. ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∨∨ ❪G1,L1,T1❫ ≅ ❪G2,L2,T2❫
+ | ❪G1,L1,T1❫ ≻ ❪G2,L2,T2❫.
+#G1 #G2 #L1 #L2 #T1 #T2 #H
+elim (feqg_dec sfull … G1 G2 L1 L2 T1 T2) //
+[ /2 width=1 by or_introl/
+| /4 width=1 by fpbq_fneqx_inv_fpb, or_intror/
+]