-lemma lveq_inv_pair_pair: ∀I1,I2,K1,K2,V1,V2,n1,n2. K1.ⓑ{I1}V1 ≋ⓧ*[n1, n2] K2.ⓑ{I2}V2 →
- ∧∧ K1 ≋ⓧ*[0, 0] K2 & 0 = n1 & 0 = n2.
+lemma lveq_inv_pair_pair: ∀I1,I2,K1,K2,V1,V2,n1,n2. K1.ⓑ{I1}V1 ≋ⓧ*[n1,n2] K2.ⓑ{I2}V2 →
+ ∧∧ K1 ≋ⓧ*[0,0] K2 & 0 = n1 & 0 = n2.