(* *)
(**************************************************************************)
-include "basic_2/relocation/lex_length.ma".
+include "static_2/relocation/lex_length.ma".
include "basic_2/rt_computation/lprs.ma".
(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
(* Forward lemmas with length for local environments ************************)
-lemma lprs_fwd_length (h) (G): â\88\80L1,L2. â¦\83G, L1â¦\84 â\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-.