Goal:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   (eqb_of_listable x y = true <-> x = y ->
    reflectProp (x = y) (eqb_of_listable x y))


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

Goals:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   (true = true <-> x = y -> reflectProp (x = y) true)

  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   (false = true <-> x = y -> reflectProp (x = y) false)


DEBUG:Going to execute:
case
DEBUG LTAC Evaluated term: eqb_of_listable

Goals:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   (true = true <-> x = y -> reflectProp (x = y) true)

  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   (false = true <-> x = y -> reflectProp (x = y) false)


DEBUG:Going to execute:
<coq-core.plugins.ssreflect::ssrcase@1>

Goals:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   ((true = true -> x = y) ->
    (x = y -> true = true) -> reflectProp (x = y) true)

  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   ((false = true -> x = y) ->
    (x = y -> false = true) -> reflectProp (x = y) false)


DEBUG:Going to execute:
constructor

Goals:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   ((true = true -> x = y) ->
    (x = y -> true = true) -> reflectProp (x = y) true)

  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  ============================
   ((false = true -> x = y) ->
    (x = y -> false = true) -> reflectProp (x = y) false)


DEBUG:Going to execute:
<coq-core.plugins.ltac::constructor@0>

Goals:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  a : true = true -> x = y
  b : x = y -> true = true
  ============================
   (x = y)

  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  a : false = true -> x = y
  b : x = y -> false = true
  ============================
   (x <> y)


DEBUG:Going to execute:
auto

Goals:
  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  a : true = true -> x = y
  b : x = y -> true = true
  ============================
   (x = y)

  
  T : Type
  Listable_T : Listable T
  FinitelyListable_T : FinitelyListable T
  x : T
  y : T
  a : false = true -> x = y
  b : x = y -> false = true
  ============================
   (x <> y)


DEBUG:Going to execute:
<coq-core.plugins.ltac::auto@0> $1 $2 $3