Goal:
    A : Type  n : nat  l : list A  i : nat
  ============================
   (nth_error (skipn n l) i = nth_error l (n + i))


DEBUG:Going to execute:
induction l in n, i |- *

Goals:
    A : Type  n : nat  i : nat
  ============================
   (nth_error (skipn n []) i = nth_error [] (n + i))

  
  A : Type
  n : nat
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (skipn n (a :: l)) i = nth_error (a :: l) (n + i))


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

Goals:
    A : Type  i : nat
  ============================
   (nth_error (skipn 0 []) i = nth_error [] (0 + i))

    A : Type  n : nat  i : nat
  ============================
   (nth_error (skipn (S n) []) i = nth_error [] (S n + i))

  
  A : Type
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (skipn 0 (a :: l)) i = nth_error (a :: l) (0 + i))

  
  A : Type
  n : nat
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (skipn (S n) (a :: l)) i = nth_error (a :: l) (S n + i))


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

Goals:
    A : Type  i : nat
  ============================
   (nth_error [] i = nth_error [] i)

    A : Type  n : nat  i : nat
  ============================
   (nth_error [] i = None)

  
  A : Type
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (a :: l) i = nth_error (a :: l) i)

  
  A : Type
  n : nat
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (skipn n l) i = nth_error l (n + i))


DEBUG:Going to execute:
auto

Goals:
    A : Type  i : nat
  ============================
   (nth_error [] i = nth_error [] i)

    A : Type  n : nat  i : nat
  ============================
   (nth_error [] i = None)

  
  A : Type
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (a :: l) i = nth_error (a :: l) i)

  
  A : Type
  n : nat
  a : A
  l : list A
  i : nat
  IHl : ∀ n i : nat, nth_error (skipn n l) i = nth_error l (n + i)
  ============================
   (nth_error (skipn n l) i = nth_error l (n + i))


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