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


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

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

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

    m : Z
  ============================
   ({None <= Some m} + {Some m < 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