(* WEIGHT OF A TERM *********************************************************)
let rec tw T ≝ match T with
-[ TSort _ ⇒ 1
-| TLRef _ ⇒ 1
+[ TAtom _ ⇒ 1
| TPair _ V T ⇒ tw V + tw T + 1
].
axiom tw_wf_ind: ∀R:term→Prop.
(∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
∀T. R T.
+
+(* Basic-1: removed theorems 11:
+ wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
+ weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
+ removed local theorems 1: q_ind
+*)