(* Advanced inversion lemmas ************************************************)
lemma lfpx_inv_bind_void: ∀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.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ.
+ â\88§â\88§ â¦\83G, L1â¦\84 â\8a¢ â¬\88[h, V] L2 & ⦃G, L1.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ.
/2 width=3 by lfxs_inv_bind_void/ qed-.
(* Advanced forward lemmas **************************************************)