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