+/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-.