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


DEBUG:Going to execute:
destruct n; try reflexivity