Make C-c C-s deal with multi-line type declarations

Now there's some heuristics to find the right place to put the added
clause in the case of definitions like

    plusComm : (n, m : Nat) ->
               n + m = m + n

Instead of just putting the clause on the next line, like:

    plusComm : (n, m : Nat) ->
    plusComm n m = ?plusComm_rhs
               n + m = m + n

it finds a line that is indented the same or less than the original, producing:

    plusComm : (n, m : Nat) ->
               n + m = m + n
    plusComm n m = ?plusComm_rhs