| Who Cites reverse? |
|
reverse | Def rev(as) == Case of as; nil nil ; a.as' rev(as') @ [a] (recursive) |
| | Thm* T:Type, as:T List. rev(as) T List |
|
append | Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive) |
| | Thm* T:Type, as,bs:T List. (as @ bs) T List |