Goal:
    n : t  m : t
  ============================
   (n <= m -> m <= n -> n = m)


DEBUG:Going to execute:
destruct n, m

Goals:
    z : Z  z0 : Z
  ============================
   (Some z <= Some z0 -> Some z0 <= Some z -> Some z = Some z0)

    z : Z
  ============================
   (Some z <= None -> None <= Some z -> Some z = None)

    z : Z
  ============================
   (None <= Some z -> Some z <= None -> None = Some z)

  
  ============================
   (None <= None -> None <= None -> None = None)


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: m
DEBUG LTAC Evaluated term: m

Goals:
    z : Z  z0 : Z
  ============================
   ((z <= z0)%Z -> (z0 <= z)%Z -> Some z = Some z0)

    z : Z
  ============================
   (False -> True -> Some z = None)

    z : Z
  ============================
   (True -> False -> None = Some z)

  
  ============================
   (True -> True -> None = None)


DEBUG:Going to execute:
try easy