-inductive jsx (h) (G): relation lenv ≝
-| jsx_atom: jsx h G (⋆) (⋆)
-| jsx_bind: ∀I,K1,K2. jsx h G K1 K2 →
- jsx h G (K1.ⓘ{I}) (K2.ⓘ{I})
-| jsx_pair: ∀I,K1,K2,V. jsx h G K1 K2 →
- G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ → jsx h G (K1.ⓑ{I}V) (K2.ⓧ)
+inductive jsx (G): relation lenv ≝
+| jsx_atom: jsx G (⋆) (⋆)
+| jsx_bind: ∀I,K1,K2. jsx G K1 K2 →
+ jsx G (K1.ⓘ[I]) (K2.ⓘ[I])
+| jsx_pair: ∀I,K1,K2,V. jsx G K1 K2 →
+ G ⊢ ⬈*𝐒[V] K2 → jsx G (K1.ⓑ[I]V) (K2.ⓧ)