(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
-let rec lw L ≝ match L with
+rec definition lw L ≝ match L with
[ LAtom ⇒ 0
-| LPair L _ V ⇒ lw L + #{V}
+| LPair L _ V ⇒ lw L + ♯{V}
].
interpretation "weight (local environment)" 'Weight L = (lw L).
(* Basic properties *********************************************************)
-lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
-/3 width=1/ qed.
+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_1: removed theorems 2: clt_cong clt_head clt_thead *)
+(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *)
+(* Basic_1: removed local theorems 1: clt_wf__q_ind *)
(* Basic_1: note: clt_thead should be renamed clt_ctail *)