Goal:
    A : Type  v : A  x : nat  H : None = Some v
  ============================
   False


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

Debug:
  
  A : Type
  v : A
  ============================
  False → ∃ _ : nat, None = Some v
Debug:
  
  A : Type
  v : A
  H : False
  ============================
  ∃ _ : nat, None = Some v