(* Forward lemmas with restricted refinement for local environments *********)
-lemma jsx_fwd_lsubr (h) (G): ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2.
+lemma jsx_fwd_lsubr (h) (G):
+ ∀L1,L2. G ⊢ L1 ⊒[h] L2 → L1 ⫃ L2.
#h #G #L1 #L2 #H elim H -L1 -L2
/2 width=1 by lsubr_bind, lsubr_unit/
qed-.