-lemma lpr_fpb (h) (G) (T): ∀L1,L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → (L1 ≛[T] L2 → ⊥) →
- ⦃G,L1,T⦄ ≻[h] ⦃G,L2,T⦄.
-/3 width=1 by fpb_lpx, lpr_fwd_lpx/ qed.
+lemma rpx_fpb (G) (T):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T] L2 → ❪G,L1,T❫ ≽ ❪G,L2,T❫.
+/2 width=5 by fpb_intro/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma fpb_inv_gen (G1) (L1) (T1) (G2) (L2) (T2):
+ ❪G1,L1,T1❫ ≽ ❪G2,L2,T2❫ →
+ ∃∃L,T. ❪G1,L1,T1❫ ⬂⸮ ❪G2,L,T❫ & ❪G2,L❫ ⊢ T ⬈ T2 & ❪G2,L❫ ⊢ ⬈[T] L2.
+// qed-.
+
+(* Basic_2A1: removed theorems 2:
+ fpbq_fpbqa fpbqa_inv_fpbq
+*)