-lemma reqx_inv_lref_pair_sn: โL1,L2,i. L1 โ[#i] L2 โ โI,K1,V1. โฉ*[i] L1 โ K1.โ[I]V1 โ
- โโK2,V2. โฉ*[i] L2 โ K2.โ[I]V2 & K1 โ[V1] K2 & V1 โ V2.
+lemma reqx_inv_lref_pair_sn: โL1,L2,i. L1 โ[#i] L2 โ โI,K1,V1. โฉ[i] L1 โ K1.โ[I]V1 โ
+ โโK2,V2. โฉ[i] L2 โ K2.โ[I]V2 & K1 โ[V1] K2 & V1 โ V2.