implement rows and prove it terminates

That is, just set up a stupid result for rows
and get the obligations to go thru; only one
is interesting: the one that shows that the
recursive call is okay

To make this work, extend drop's type so you get
enough information from it