(* *)
(**************************************************************************)
-include "basic_2/syntax/term_weight.ma".
+include "basic_2/syntax/bind_weight.ma".
include "basic_2/syntax/lenv.ma".
(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
rec definition lw L ≝ match L with
-[ LAtom ⇒ 0
-| LPair L _ V ⇒ lw L + ♯{V}
+[ LAtom ⇒ 0
+| LBind L I ⇒ lw L + ♯{I}
].
interpretation "weight (local environment)" 'Weight L = (lw L).
(* Basic properties *********************************************************)
-lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}.
-/3 width=1 by lt_plus_to_minus_r, monotonic_lt_plus_r/ qed.
+(* Basic_2A1: uses: lw_pair *)
+lemma lw_bind: ∀I,L. ♯{L} < ♯{L.ⓘ{I}}.
+normalize /2 width=1 by monotonic_le_plus_r/ qed.
(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *)
(* Basic_1: removed local theorems 1: clt_wf__q_ind *)