include "static_2/relocation/lex_length.ma".
include "basic_2/rt_transition/lpx.ma".
-(* UNBOUND PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS ***************)
+(* EXTENDED PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS **************)
(* 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 (G):
+ ∀L1,L2. ❪G,L1❫ ⊢ ⬈ L2 → |L1| = |L2|.
/2 width=2 by lex_fwd_length/ qed-.