Goal:
    X : Type  f : X → bool  a : X  xs : list X  IHxs : #|filter f xs| ≤ #|xs|
  ============================
   (#|filter f (a :: xs)| ≤ #|a :: xs|)


DEBUG:Going to execute:
idtac