-inductive lsubsx (h) (o) (G): rtmap → relation lenv ≝
-| lsubsx_atom: ∀f. lsubsx h o G f (⋆) (⋆)
-| lsubsx_push: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
- lsubsx h o G (⫯f) (K1.ⓘ{I}) (K2.ⓘ{I})
-| lsubsx_unit: ∀f,I,K1,K2. lsubsx h o G f K1 K2 →
- lsubsx h o G (↑f) (K1.ⓤ{I}) (K2.ⓧ)
-| lsubsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ →
- lsubsx h o G f K1 K2 → lsubsx h o G (↑f) (K1.ⓑ{I}V) (K2.ⓧ)
+inductive lsubsx (h) (G): rtmap → relation lenv ≝
+| lsubsx_atom: ∀f. lsubsx h G f (⋆) (⋆)
+| lsubsx_push: ∀f,I,K1,K2. lsubsx h G f K1 K2 →
+ lsubsx h G (⫯f) (K1.ⓘ{I}) (K2.ⓘ{I})
+| lsubsx_unit: ∀f,I,K1,K2. lsubsx h G f K1 K2 →
+ lsubsx h G (↑f) (K1.ⓤ{I}) (K2.ⓧ)
+| lsubsx_pair: ∀f,I,K1,K2,V. G ⊢ ⬈*[h, V] 𝐒⦃K2⦄ →
+ lsubsx h G f K1 K2 → lsubsx h G (↑f) (K1.ⓑ{I}V) (K2.ⓧ)