].
interpretation "weight (binder for local environments)" 'Weight I = (bw I).
(* Basic properties *********************************************************)
].
interpretation "weight (binder for local environments)" 'Weight I = (bw I).
(* Basic properties *********************************************************)