include "Basic-2/grammar/term.ma".
-(* WEIGHT *******************************************************************)
+(* WEIGHT OF A TERM *********************************************************)
-(* the weight of a term *)
let rec tw T ≝ match T with
[ TSort _ ⇒ 1
| TLRef _ ⇒ 1
interpretation "weight (term)" 'Weight T = (tw T).
-axiom tw_wf_ind: ∀P:term→Prop.
- (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
- ∀T. P T.
+(* Basic properties *********************************************************)
+
+axiom tw_wf_ind: ∀R:term→Prop.
+ (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
+ ∀T. R T.