L:T List. |
|(L)
0T:Type, L:T List. ||(L) 
T:Type, L:T List. ||(L) 
T:Type, L:T List. ||(L) | == (letrec l L = (Case of L; nil 
0 ; h.t 1+l(t)) )
is mentioned by
| Thm* L:T List. ||(L)0 | [list_length_non_negative] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length_int] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length_nat] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length] |