Goal:
    n : t
  ============================
   (max n None = n)


DEBUG:Going to execute:
destruct n; simpl