Goal:
    n : t  m : t  k : t  H : max n m = k
  ============================
   (n = k \/ m = k)


DEBUG:Going to execute:
destruct n, m

Goals:
    z : Z  z0 : Z  k : t  H : max (Some z) (Some z0) = k
  ============================
   (Some z = k \/ Some z0 = k)

    z : Z  k : t  H : max (Some z) None = k
  ============================
   (Some z = k \/ None = k)

    z : Z  k : t  H : max None (Some z) = k
  ============================
   (None = k \/ Some z = k)

    k : t  H : max None None = k
  ============================
   (None = k \/ None = k)


DEBUG:Going to execute:
simpl in *
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: m
DEBUG LTAC Evaluated term: m