(* Forward lemmas with length for local environments ************************)
-lemma lpx_fwd_length (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → |L1| = |L2|.
+lemma lpx_fwd_length (h) (G): ∀L1,L2. ⦃G,L1⦄ ⊢ ⬈[h] L2 → |L1| = |L2|.
/2 width=2 by lex_fwd_length/ qed-.