-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_fsge_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_fsge_comp, lfxs_bind_dx_split_void/ qed-.
+
+lemma lfpx_tdeq_conf: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpx h G).
+/2 width=5 by tdeq_lfxs_conf/ qed-.
+
+lemma lfpx_tdeq_div: ∀h,o,T1,T2. T1 ≛[h, o] T2 →
+ ∀G,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T2] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T1] L2.
+/2 width=5 by tdeq_lfxs_div/ qed-.