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])