(* Basic properties *********************************************************)
-(* Basic_1: was: tweight_lt *)
lemma tw_pos: ∀T. 1 ≤ ♯{T}.
#T elim T -T //
qed.
-
-(* 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
-*)
-(* Basic_1: removed local theorems 1: q_ind *)