inductive lsuba: relation lenv ≝
| lsuba_atom: lsuba (⋆) (⋆)
| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)
inductive lsuba: relation lenv ≝
| lsuba_atom: lsuba (⋆) (⋆)
| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)