+
+(* Inversion lemmas with proper parallel rst-computation for closures *******)
+
+lemma fsb_fpbg_refl_false (h) (o) (G) (L) (T):
+ ≥[h,o] 𝐒⦃G, L, T⦄ → ⦃G, L, T⦄ >[h,o] ⦃G, L, T⦄ → ⊥.
+#h #o #G #L #T #H
+@(fsb_ind_fpbg … H) -G -L -T #G1 #L1 #T1 #_ #IH #H
+/2 width=5 by/
+qed-.