(* *)
(**************************************************************************)
+include "basic_2/notation/functions/weight_1.ma".
include "basic_2/grammar/term.ma".
(* WEIGHT OF A TERM *********************************************************)
(* Basic properties *********************************************************)
(* Basic_1: was: tweight_lt *)
-lemma tw_pos: ∀T. 1 ≤ #{T}.
+lemma tw_pos: ∀T. 1 ≤ ♯{T}.
#T elim T -T //
qed.