Goal:
    A : Type  n : nat  l : list A  l' : list A
  ============================
   (n ≤ #|l| → skipn n (l ++ l') = skipn n l ++ l')


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

Goals:
    A : Type  n : nat  l' : list A
  ============================
   (n ≤ #|[]| → skipn n ([] ++ l') = skipn n [] ++ l')

  
  A : Type
  n : nat
  a : A
  l : list A
  l' : list A
  IHl : ∀ (n : nat) (l' : list A),
          n ≤ #|l| → skipn n (l ++ l') = skipn n l ++ l'
  ============================
   (n ≤ #|a :: l| → skipn n ((a :: l) ++ l') = skipn n (a :: l) ++ l')


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

Goals:
    A : Type  n : nat  l' : list A
  ============================
   (n ≤ 0 → skipn n l' = skipn n [] ++ l')

  
  A : Type
  n : nat
  a : A
  l : list A
  l' : list A
  IHl : ∀ (n : nat) (l' : list A),
          n ≤ #|l| → skipn n (l ++ l') = skipn n l ++ l'
  ============================
   (n ≤ S #|l| → skipn n (a :: l ++ l') = skipn n (a :: l) ++ l')


DEBUG:Going to execute:
auto

Goals:
    A : Type  n : nat  l' : list A
  ============================
   (n ≤ 0 → skipn n l' = skipn n [] ++ l')

  
  A : Type
  n : nat
  a : A
  l : list A
  l' : list A
  IHl : ∀ (n : nat) (l' : list A),
          n ≤ #|l| → skipn n (l ++ l') = skipn n l ++ l'
  ============================
   (n ≤ S #|l| → skipn n (a :: l ++ l') = skipn n (a :: l) ++ l')


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