T:Type, L:T List, x:T. null(L)  last([x / L]) = last(L)

By:	Unfold `last` 0 THEN Reduce 0 THEN Assert (||L||>0) THENL [RW assert_pushdownC -1 THEN Easy ;RWO Thm* a:T, as:T List, i:. 0<i  i||as||  [a / as][i] = as[(i-1)] 0]

None

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html