-inductive lsuba: relation lenv ≝
-| lsuba_atom: lsuba (⋆) (⋆)
-| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsuba_abbr: ∀L1,L2,W,V,A. L1 ⊢ ⓝW.V ⁝ A → L2 ⊢ W ⁝ A →
- lsuba L1 L2 → lsuba (L1.ⓓⓝW.V) (L2.ⓛW)
+inductive lsuba (G:genv): relation lenv ≝
+| lsuba_atom: lsuba G (⋆) (⋆)
+| lsuba_pair: ∀I,L1,L2,V. lsuba G L1 L2 → lsuba G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsuba_abbr: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A →
+ lsuba G L1 L2 → lsuba G (L1.ⓓⓝW.V) (L2.ⓛW)