inductive lsuba (G:genv): relation lenv ≝
| lsuba_atom: lsuba G (⋆) (⋆)
| lsuba_bind: ∀I,L1,L2. lsuba G L1 L2 → lsuba G (L1.ⓘ{I}) (L2.ⓘ{I})
inductive lsuba (G:genv): relation lenv ≝
| lsuba_atom: lsuba G (⋆) (⋆)
| lsuba_bind: ∀I,L1,L2. lsuba G L1 L2 → lsuba G (L1.ⓘ{I}) (L2.ⓘ{I})