Goal:
  
  A : Type
  n : nat
  a : A
  l : list A
  IHl : ∀ n : nat, #|firstn n l| = n → n ≤ #|l|
  ============================
   (#|firstn n (a :: l)| = n → n ≤ S #|l|)


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

Goals:
    A : Type  n : nat
  ============================
   (#|firstn n []| = n → n ≤ 0)

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


DEBUG:Going to execute:
destruct n

Goals:
    A : Type
  ============================
   (#|firstn 0 []| = 0 → 0 ≤ 0)

    A : Type  n : nat
  ============================
   (#|firstn (S n) []| = S n → S n ≤ 0)

  
  A : Type
  a : A
  l : list A
  IHl : ∀ n : nat, #|firstn n l| = n → n ≤ #|l|
  ============================
   (#|firstn 0 (a :: l)| = 0 → 0 ≤ S #|l|)

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


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

Goals:
    A : Type
  ============================
   (0 = 0 → 0 ≤ 0)

    A : Type  n : nat
  ============================
   (0 = S n → S n ≤ 0)

  
  A : Type
  a : A
  l : list A
  IHl : ∀ n : nat, #|firstn n l| = n → n ≤ #|l|
  ============================
   (0 = 0 → 0 ≤ S #|l|)

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


DEBUG:Going to execute:
auto with arith