].
interpretation "weight (local environment)" 'Weight L = (lw L).
(* Basic properties *********************************************************)
].
interpretation "weight (local environment)" 'Weight L = (lw L).
(* Basic properties *********************************************************)