Goal:
  
  ============================
   (Irreflexive lt)


DEBUG:Going to execute:
intros []

Goals:
  
  ============================
   (complement lt true true)

  
  ============================
   (complement lt false false)


DEBUG:Going to execute:
cbn

Goals:
  
  ============================
   (complement lt true true)

  
  ============================
   (complement lt false false)


DEBUG:Going to execute:
unfold lt, complement

Goals:
  
  ============================
   (False -> False)

  
  ============================
   (false = true -> False)


DEBUG:Going to execute:
congruence

Goals:
  
  ============================
   (False -> False)

  
  ============================
   (false = true -> False)


DEBUG:Going to execute:
<coq-core.plugins.cc::cc@0> $1