Goal:
    A : Type  m : nat  x : A
  ============================
   (∀ (n : nat) (l : list A),
      nth_error (firstn n l) m = Some x → nth_error l m = Some x)


DEBUG:Going to execute:
induction m

Goals:
    A : Type  x : A
  ============================
   (∀ (n : nat) (l : list A),
      nth_error (firstn n l) 0 = Some x → nth_error l 0 = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  ============================
   (∀ (n : nat) (l : list A),
      nth_error (firstn n l) (S m) = Some x → nth_error l (S m) = Some x)


DEBUG:Going to execute:
intros n l H
DEBUG LTAC Evaluated term: m

Goals:
  
  A : Type
  x : A
  n : nat
  l : list A
  H : nth_error (firstn n l) 0 = Some x
  ============================
   (nth_error l 0 = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  n : nat
  l : list A
  H : nth_error (firstn n l) (S m) = Some x
  ============================
   (nth_error l (S m) = Some x)


DEBUG:Going to execute:
destruct n, l

Goals:
    A : Type  x : A  H : nth_error (firstn 0 []) 0 = Some x
  ============================
   (nth_error [] 0 = Some x)

  
  A : Type
  x : A
  a : A
  l : list A
  H : nth_error (firstn 0 (a :: l)) 0 = Some x
  ============================
   (nth_error (a :: l) 0 = Some x)

    A : Type  x : A  n : nat  H : nth_error (firstn (S n) []) 0 = Some x
  ============================
   (nth_error [] 0 = Some x)

  
  A : Type
  x : A
  n : nat
  a : A
  l : list A
  H : nth_error (firstn (S n) (a :: l)) 0 = Some x
  ============================
   (nth_error (a :: l) 0 = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  H : nth_error (firstn 0 []) (S m) = Some x
  ============================
   (nth_error [] (S m) = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  a : A
  l : list A
  H : nth_error (firstn 0 (a :: l)) (S m) = Some x
  ============================
   (nth_error (a :: l) (S m) = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  n : nat
  H : nth_error (firstn (S n) []) (S m) = Some x
  ============================
   (nth_error [] (S m) = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  n : nat
  a : A
  l : list A
  H : nth_error (firstn (S n) (a :: l)) (S m) = Some x
  ============================
   (nth_error (a :: l) (S m) = Some x)


DEBUG:Going to execute:
cbn in *
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: n
DEBUG LTAC Evaluated term: l
DEBUG LTAC Evaluated term: l

Goals:
    A : Type  x : A  H : None = Some x
  ============================
   (None = Some x)

    A : Type  x : A  a : A  l : list A  H : None = Some x
  ============================
   (Some a = Some x)

    A : Type  x : A  n : nat  H : None = Some x
  ============================
   (None = Some x)

    A : Type  x : A  n : nat  a : A  l : list A  H : Some a = Some x
  ============================
   (Some a = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  H : None = Some x
  ============================
   (None = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  a : A
  l : list A
  H : None = Some x
  ============================
   (nth_error l m = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  n : nat
  H : None = Some x
  ============================
   (None = Some x)

  
  A : Type
  m : nat
  x : A
  IHm : ∀ (n : nat) (l : list A),
          nth_error (firstn n l) m = Some x → nth_error l m = Some x
  n : nat
  a : A
  l : list A
  H : nth_error (firstn n l) m = Some x
  ============================
   (nth_error l m = Some x)


DEBUG:Going to execute:
try (solve [ inversion H ])