∧∧ |L1| = |L2| & |L1| = |L|
& (∀I1,I2,I,K1,K2,K,V1,V2,V,i.
⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → ⬇[i] L ≡ K.ⓑ{I}V → ∨∨
∧∧ |L1| = |L2| & |L1| = |L|
& (∀I1,I2,I,K1,K2,K,V1,V2,V,i.
⬇[i] L1 ≡ K1.ⓑ{I1}V1 → ⬇[i] L2 ≡ K2.ⓑ{I2}V2 → ⬇[i] L ≡ K.ⓑ{I}V → ∨∨