Goal:
    n : t  m : t
  ============================
   ({n <= m} + {~ n <= m})


DEBUG:Going to execute:
destruct n as [n| ], m as [m| ]

Goals:
    n : Z  m : Z
  ============================
   ({Some n <= Some m} + {~ Some n <= Some m})

    n : Z
  ============================
   ({Some n <= None} + {~ Some n <= None})

    m : Z
  ============================
   ({None <= Some m} + {~ None <= Some m})

  
  ============================
   ({None <= None} + {~ None <= None})


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