-(*** height of T's syntactic tree ***)
-
-let rec t_len T \def
- match T with
- [(TVar n) \Rightarrow (S O)
- |(TFree X) \Rightarrow (S O)
- |Top \Rightarrow (S O)
- |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))
- |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))].
-