(* Forward lemmas with length for local environments ************************)
-lemma lprs_fwd_length (h) (G): â\88\80L1,L2. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h] L2 → |L1| = |L2|.
+lemma lprs_fwd_length (h) (G): â\88\80L1,L2. â\9d¨G,L1â\9d© â\8a¢ â\9e¡*[h,0] L2 → |L1| = |L2|.
/2 width=2 by lex_fwd_length/ qed-.