-lemma rdeq_inv_lref_pair_sn: â\88\80L1,L2,i. L1 â\89\9b[#i] L2 â\86\92 â\88\80I,K1,V1. â¬\87*[i] L1 ≘ K1.ⓑ{I}V1 →
- â\88\83â\88\83K2,V2. â¬\87*[i] L2 ≘ K2.ⓑ{I}V2 & K1 ≛[V1] K2 & V1 ≛ V2.
+lemma rdeq_inv_lref_pair_sn: â\88\80L1,L2,i. L1 â\89\9b[#i] L2 â\86\92 â\88\80I,K1,V1. â\87©*[i] L1 ≘ K1.ⓑ{I}V1 →
+ â\88\83â\88\83K2,V2. â\87©*[i] L2 ≘ K2.ⓑ{I}V2 & K1 ≛[V1] K2 & V1 ≛ V2.