Never heard of Agda, thanks for the pointer. From what I read, it seems that Agda proofs are written declaratively, rather than interactively using tactics as in Coq. From experience, Coq's tactic-based proof system is very nice as it "unravels" the proof term in a way that makes it more manageable than balancing lambda terms in one's head.
Regarding the question of totality on slide 40, a naïve analysis would say that the deconstruction "let (y : ys) =" could fail (if the list returned from reverse were empty), and thus the function would not be total. Of course this is not the case, since reversing a non-empty list returns a non-empty list, but this requires that reverse be dependently typed.
(Slightly off-topic: the Mercury logic programming language supports just the right amount of dependency to allow this specification of reverse, and would deduce totality for this function.)
Back on topic, yes, most practical functions can be rewritten to be structurally recursive. The most brain-dead easy way is add a "time-to-live" argument to the recursive function. This argument is a Peano number initially set to a value higher than the expected number of recurrences. (In the example from the slides, one could choose the total number of windows on the screen.) The function is then modified to decrement the time-to-live argument on each recurrence, and to return a dummy value should the time-to-live reach zero. It's then trivial to prove that the function terminates, and usually easy to prove that it does what it's supposed to do before the time-to-live zeros out.