lemma lfpx_fwd_flat_dx: ∀h,I,G,L1,L2,V,T.
⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
/2 width=3 by lfxs_fwd_flat_dx/ qed-.
lemma lfpx_fwd_flat_dx: ∀h,I,G,L1,L2,V,T.
⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2.
/2 width=3 by lfxs_fwd_flat_dx/ qed-.