-lemma lfpx_bind_dx_split: ∀h,o,p,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 →
- ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≡[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
-/3 width=5 by lfpx_frees_conf, lfxs_bind_dx_split/ qed-.
+lemma lfpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀o,p.
+ ∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
+/3 width=5 by lfpx_fsle_comp, lfxs_bind_dx_split/ qed-.
+
+lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 → ∀o,p,I,V.
+ ∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≛[h, o, T] L2.
+/3 width=5 by lfpx_fsle_comp, lfxs_bind_dx_split_void/ qed-.