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


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