Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)

Thm* A:Type, l:A*. ||l||

Thm* ||nil||

Def rev(as) == Case of as; nil nil ; a.as' rev(as') @ [a] (recursive)

Thm* T:Type, as:T*. rev(as) T*

Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)

Thm* T:Type, as,bs:T*. (as @ bs) T*