Filtering a list returns a list that is never bigger

vect_filter.idr

-- If the length is < n+1, it is less than n+2
weakenPair: (p: Fin n ** Vect (finToNat p) a) -> (p1: Fin (S n) ** Vect (finToNat p1) a)
weakenPair (FZ ** v) = (FZ ** v)
weakenPair (FS k ** v) = believe_me (FS k ** v) -- How to prove this branch?

filt : Vect n a -> (fn: a -> Bool) -> (p: Fin (S n) ** Vect (finToNat p) a)
filt [] _ = (0 ** [])
filt (x :: xs) fn with (filt xs fn)
  | (p' ** xs') = if (fn x) then ((shift 1 p') ** (x :: xs')) else weakenPair (p' ** xs')

How about this:

filtersmall : (a -> Bool) -> Vect n a -> (p ** (Vect p a, LTE p n))
filtersmall f [] = (0 ** ([], LTEZero))
filtersmall f (x :: xs) with (filtersmall f xs)
  filtersmall f (x :: xs) | (p ** (xs', prf))
         = case f x of
                False => (_ ** (xs', lteSuccRight prf))
                True => (_ ** (x :: xs', LTESucc prf))

As a general rule, using functions in a return type can lead to difficulties, so if you can represent things as a data structure instead (e.g. LTE here) things can become easier.