Goal:
    G : t  HI : invariants  x : VSet.elt
  ============================
   (Some 0 = Some 0)


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

Goals:
    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (ssrbool.reflect (Some (Z.pos p) = Some 0) false)

    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (ssrbool.reflect (Some (Z.neg p) = Some 0) false)

    G : t  HI : invariants  x : VSet.elt
  ============================
   (ssrbool.reflect (None = Some 0) false)


DEBUG:Going to execute:
constructor

Goals:
    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (ssrbool.reflect (Some (Z.pos p) = Some 0) false)

    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (ssrbool.reflect (Some (Z.neg p) = Some 0) false)

    G : t  HI : invariants  x : VSet.elt
  ============================
   (ssrbool.reflect (None = Some 0) false)


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

Goals:
    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (Some (Z.pos p) <> Some 0)

    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (Some (Z.neg p) <> Some 0)

    G : t  HI : invariants  x : VSet.elt
  ============================
   (None <> Some 0)


DEBUG:Going to execute:
discriminate

Goals:
    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (Some (Z.pos p) <> Some 0)

    G : t  HI : invariants  x : VSet.elt  p : positive
  ============================
   (Some (Z.neg p) <> Some 0)

    G : t  HI : invariants  x : VSet.elt
  ============================
   (None <> Some 0)


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