Goal:
  
  A : Type
  n : nat
  m : nat
  IHm : ∀ (n : nat) (l : list A), skipn n (skipn m l) = skipn (m + n) l
  ============================
   (skipn n (skipn (S m) []) = skipn (S (m + n)) [])


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

Goals:
  
  A : Type
  m : nat
  IHm : ∀ (n : nat) (l : list A), skipn n (skipn m l) = skipn (m + n) l
  ============================
   (skipn 0 (skipn (S m) []) = skipn (S (m + 0)) [])

  
  A : Type
  n : nat
  m : nat
  IHm : ∀ (n : nat) (l : list A), skipn n (skipn m l) = skipn (m + n) l
  ============================
   (skipn (S n) (skipn (S m) []) = skipn (S (m + S n)) [])


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

Goals:
  
  A : Type
  m : nat
  IHm : ∀ (n : nat) (l : list A), skipn n (skipn m l) = skipn (m + n) l
  ============================
   (skipn 0 (skipn (S m) []) = skipn (S (m + 0)) [])

  
  A : Type
  n : nat
  m : nat
  IHm : ∀ (n : nat) (l : list A), skipn n (skipn m l) = skipn (m + n) l
  ============================
   (skipn (S n) (skipn (S m) []) = skipn (S (m + S n)) [])


DEBUG:Going to execute:
fun => <coq-core.plugins.ltac::reflexivity@0>