Write more idiomatic Idris

[yurrriq]

While this is a translation of a book written for/in Coq, we should use idiomatic Idris whenever possible.

[clayrat]

As a reminder, we should try replacing rewrites with dependent pattern matching where appropriate.

[yurrriq]

This is a broader issue, but let's get it right for the first ten chapters and document some examples and lessons learned.

[clayrat]

Look for places where match application (http://docs.idris-lang.org/en/latest/reference/misc.html#match-application) could be introduced/used. Maybe we could fix some of the bigger replaces with it?