T:Type, L:T List. ||L|| 
T:Type, L:T List. |
|(L) T:Type, L:T List. ||(L) T:Type. || (T List)
== {i:
| 0
i }
is mentioned by
| Thm* T:Type, L:T List. ||L|| | [length_wf_nat] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length_nat] |
| Thm* T:Type, L:T List. ||(L) | [apply_wf_list_length] |
| Thm* T:Type. || (T List) | [list_length_wf_nat] |
In prior sections: int 1 bool 1 int 2 list 1