Goal:
    A : Type  v : A
  ============================
   ((∃ _ : nat, None = Some v) ↔ False)


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

Debug:
  
  A : Type
  v : A
  ============================
  (∃ _ : nat, None = Some v) ↔ False
Debug:
  
  A : Type
  v : A
  ============================
  (∃ _ : nat, None = Some v) → False
Debug:
  
  A : Type
  v : A
  H : ∃ _ : nat, None = Some v
  ============================
  False
Debug:
  
  A : Type
  v : A
  x : nat
  H : None = Some v
  ============================
  False
Debug:
  
  A : Type
  v : A
  x : nat
  H : None = Some v
  ============================
  False