Goal:
    n : t  m : t  p : t
  ============================
   (max (n + p) (m + p) = max n m + p)


DEBUG:Going to execute:
destruct n, m, p

Goals:
    z : Z  z0 : Z  z1 : Z
  ============================
   (max (Some z + Some z1) (Some z0 + Some z1) =
    max (Some z) (Some z0) + Some z1)

    z : Z  z0 : Z
  ============================
   (max (Some z + None) (Some z0 + None) = max (Some z) (Some z0) + None)

    z : Z  z0 : Z
  ============================
   (max (Some z + Some z0) (None + Some z0) = max (Some z) None + Some z0)

    z : Z
  ============================
   (max (Some z + None) (None + None) = max (Some z) None + None)

    z : Z  z0 : Z
  ============================
   (max (None + Some z0) (Some z + Some z0) = max None (Some z) + Some z0)

    z : Z
  ============================
   (max (None + None) (Some z + None) = max None (Some z) + None)

    z : Z
  ============================
   (max (None + Some z) (None + Some z) = max None None + Some z)

  
  ============================
   (max (None + None) (None + None) = max None None + None)


DEBUG:Going to execute:
try reflexivity
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: m
DEBUG LTAC Evaluated term: m
DEBUG LTAC Evaluated term: p
DEBUG LTAC Evaluated term: p
DEBUG LTAC Evaluated term: p
DEBUG LTAC Evaluated term: p