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


DEBUG:Going to execute:
induction xs