> 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 reve

> 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. You are right, I missed the deconstruction. Thanks!