/2 width=3 by ex2_intro/
qed-.
-lemma lfeq_inv_lref_bind_sn: â\88\80I1,K1,L2,i. K1.â\93\98{I1} â\89¡[#⫯i] L2 →
+lemma lfeq_inv_lref_bind_sn: â\88\80I1,K1,L2,i. K1.â\93\98{I1} â\89¡[#â\86\91i] L2 →
∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ{I2}.
/2 width=2 by lfxs_inv_lref_bind_sn/ qed-.
-lemma lfeq_inv_lref_bind_dx: â\88\80I2,K2,L1,i. L1 â\89¡[#⫯i] K2.ⓘ{I2} →
+lemma lfeq_inv_lref_bind_dx: â\88\80I2,K2,L1,i. L1 â\89¡[#â\86\91i] K2.ⓘ{I2} →
∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ{I1}.
/2 width=2 by lfxs_inv_lref_bind_dx/ qed-.