module Totality total foo : Nat -> Nat foo Z = Z