include "basic_2/static/lsubr.ma".
(* RESTRICTED REFINEMENT FOR LOCAL ENVIRONMENTS *****************************)
(* Forward lemmas with length for local environments ************************)
include "basic_2/static/lsubr.ma".
(* RESTRICTED REFINEMENT FOR LOCAL ENVIRONMENTS *****************************)
(* Forward lemmas with length for local environments ************************)