it_sum(nil) = 0
  & (l: List. mt(l)  it_sum(l) = head(l)+it_sum(tl(l)))
  & (x:, l: List. it_sum(cons(x; l)) = x+it_sum(l))

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html