Goal:
    A : Type  l : list A  n : nat  x : A
  ============================
   (nth_error l n = Some x → l ≠ [])


DEBUG:Going to execute:
destruct l, n

Goals:
    A : Type  x : A
  ============================
   (nth_error [] 0 = Some x → [] ≠ [])

    A : Type  n : nat  x : A
  ============================
   (nth_error [] (S n) = Some x → [] ≠ [])

    A : Type  a : A  l : list A  x : A
  ============================
   (nth_error (a :: l) 0 = Some x → a :: l ≠ [])

    A : Type  a : A  l : list A  n : nat  x : A
  ============================
   (nth_error (a :: l) (S n) = Some x → a :: l ≠ [])


DEBUG:Going to execute:
simpl
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: n

Goals:
    A : Type  x : A
  ============================
   (None = Some x → [] ≠ [])

    A : Type  n : nat  x : A
  ============================
   (None = Some x → [] ≠ [])

    A : Type  a : A  l : list A  x : A
  ============================
   (Some a = Some x → a :: l ≠ [])

    A : Type  a : A  l : list A  n : nat  x : A
  ============================
   (nth_error l n = Some x → a :: l ≠ [])


DEBUG:Going to execute:
congruence

Goals:
    A : Type  x : A
  ============================
   (None = Some x → [] ≠ [])

    A : Type  n : nat  x : A
  ============================
   (None = Some x → [] ≠ [])

    A : Type  a : A  l : list A  x : A
  ============================
   (Some a = Some x → a :: l ≠ [])

    A : Type  a : A  l : list A  n : nat  x : A
  ============================
   (nth_error l n = Some x → a :: l ≠ [])


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