-| lveq_pair_sn: ∀I1,I2,K1,K2,V1,n. lveq n K1 n K2 →
- lveq 0 (K1.ⓑ{I1}V1) 0 (K2.ⓘ{I2})
-| lveq_pair_dx: ∀I1,I2,K1,K2,V2,n. lveq n K1 n K2 →
- lveq 0 (K1.ⓘ{I1}) 0 (K2.ⓑ{I2}V2)
-| lveq_void_sn: ∀K1,K2,n1,n2. lveq n1 K1 n2 K2 →
- lveq (⫯n1) (K1.ⓧ) n2 K2
-| lveq_void_dx: ∀K1,K2,n1,n2. lveq n1 K1 n2 K2 →
- lveq n1 K1 (⫯n2) (K2.ⓧ)
+| lveq_bind : ∀I1,I2,K1,K2. lveq 0 K1 0 K2 →
+ lveq 0 (K1.ⓘ{I1}) 0 (K2.ⓘ{I2})
+| lveq_void_sn: ∀K1,K2,n1. lveq n1 K1 0 K2 →
+ lveq (↑n1) (K1.ⓧ) 0 K2
+| lveq_void_dx: ∀K1,K2,n2. lveq 0 K1 n2 K2 →
+ lveq 0 K1 (↑n2) (K2.ⓧ)