include "basic_2/rt_transition/lpx.ma".
(* UNBOUND PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS ***************)
(* Forward lemmas with length for local environments ************************)
include "basic_2/rt_transition/lpx.ma".
(* UNBOUND PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS ***************)
(* Forward lemmas with length for local environments ************************)