Goal:
    A : Type  n : nat  l : list A
  ============================
   (#|firstn n l| = n → n ≤ #|l|)


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

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

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


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

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:
auto with arith