Goal:
    A : Type  p : A → bool  n : nat  l : list A
  ============================
   (forallb p l → forallb p (skipn n l))


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

Goals:
    A : Type  p : A → bool  n : nat
  ============================
   (forallb p [] → forallb p (skipn n []))

  
  A : Type
  p : A → bool
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, forallb p l → forallb p (skipn n l)
  ============================
   (forallb p (a :: l) → forallb p (skipn n (a :: l)))


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

Goals:
    A : Type  p : A → bool
  ============================
   (forallb p [] → forallb p (skipn 0 []))

    A : Type  p : A → bool  n : nat
  ============================
   (forallb p [] → forallb p (skipn (S n) []))

  
  A : Type
  p : A → bool
  a : A
  l : list A
  IHl : ∀ n : nat, forallb p l → forallb p (skipn n l)
  ============================
   (forallb p (a :: l) → forallb p (skipn 0 (a :: l)))

  
  A : Type
  p : A → bool
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, forallb p l → forallb p (skipn n l)
  ============================
   (forallb p (a :: l) → forallb p (skipn (S n) (a :: l)))


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

Goals:
    A : Type  p : A → bool
  ============================
   (true → true)

    A : Type  p : A → bool  n : nat
  ============================
   (true → true)

  
  A : Type
  p : A → bool
  a : A
  l : list A
  IHl : ∀ n : nat, forallb p l → forallb p (skipn n l)
  ============================
   (p a && forallb p l → p a && forallb p l)

  
  A : Type
  p : A → bool
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, forallb p l → forallb p (skipn n l)
  ============================
   (p a && forallb p l → forallb p (skipn n l))


DEBUG:Going to execute:
try congruence