/2 width=1 by lfxs_inv_gref/ qed-.
lemma lfpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 →
- â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, V] L2 â\88§ ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V.
+ â\88§â\88§ â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, V] L2 & ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V.
/2 width=2 by lfxs_inv_bind/ qed-.
lemma lfpx_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 →
- â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, V] L2 â\88§ ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
+ â\88§â\88§ â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, V] L2 & ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
/2 width=2 by lfxs_inv_flat/ qed-.
(* Advanced inversion lemmas ************************************************)