-inductive voids: bi_relation nat lenv ≝
-| voids_atom : voids 0 (⋆) 0 (⋆)
-| voids_pair_sn: ∀I1,I2,K1,K2,V1,n. voids n K1 n K2 →
- voids 0 (K1.ⓑ{I1}V1) 0 (K2.ⓘ{I2})
-| voids_pair_dx: ∀I1,I2,K1,K2,V2,n. voids n K1 n K2 →
- voids 0 (K1.ⓘ{I1}) 0 (K2.ⓑ{I2}V2)
-| voids_void_sn: ∀K1,K2,n1,n2. voids n1 K1 n2 K2 →
- voids (⫯n1) (K1.ⓧ) n2 K2
-| voids_void_dx: ∀K1,K2,n1,n2. voids n1 K1 n2 K2 →
- voids n1 K1 (⫯n2) (K2.ⓧ)
-.