Goal:
    x : t
  ============================
   (x <= x)


DEBUG:Going to execute:
destruct x

Goals:
    z : Z
  ============================
   (Some z <= Some z)

  
  ============================
   (None <= None)


DEBUG:Going to execute:
cbn
DEBUG LTAC Evaluated term: x

Goals:
    z : Z
  ============================
   (z <= z)%Z

  
  ============================
   True


DEBUG:Going to execute:
reflexivity

Goals:
    z : Z
  ============================
   (z <= z)%Z

  
  ============================
   True


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>