| Some definitions of interest. |
|
l_member | Def (x l) == i: . i < ||l|| & x = l[i] T |
| | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
rev_implies | Def P  Q == Q  P |
| | Thm* A,B:Prop. (A  B) Prop |
|
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 |