-lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1.
- â¦\83G, L1.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88[h, T] L2.â\93\91{I}V1 →
- ∀V2. ⦃G, L1⦄ ⊢ V ⬈[h] V2 →
- â¦\83G, L1.â\93\91{I}Vâ¦\84 â\8a¢ â¬\88[h, T] L2.â\93\91{I}V2.
-/2 width=2 by lfxs_pair_repl_dx/ qed-.
+lemma lfpx_bind_repl_dx: ∀h,I,I1,G,L1,L2,T.
+ â¦\83G, L1.â\93\98{I}â¦\84 â\8a¢ â¬\88[h, T] L2.â\93\98{I1} →
+ ∀I2. ⦃G, L1⦄ ⊢ I ⬈[h] I2 →
+ â¦\83G, L1.â\93\98{I}â¦\84 â\8a¢ â¬\88[h, T] L2.â\93\98{I2}.
+/2 width=2 by lfxs_bind_repl_dx/ qed-.