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


DEBUG:Going to execute:
destruct (f a); cbn