filter.idr

all' : (a -> Bool) -> List a -> Bool
all' f [] = True
all' f (x :: xs) = f x && all' f xs
  
allLemma : f x = True -> all' f xs = True -> all' f (x :: xs) = True
allLemma p1 p2 = rewrite p1 in rewrite p2 in Refl
  
allFiltered : (f : a -> Bool) -> (xs : List a) -> all' f (filter f xs) = True
allFiltered f [] = Refl
allFiltered f (x :: xs) = lemma (allFiltered f xs) (f x) Refl where
  lemma : all' f (filter f xs) = True -> (b : Bool) -> b = f x -> all' f (filter f (x :: xs)) = True
  lemma p False p2 =
    rewrite sym p2 in p
  lemma p True p2 = rewrite sym p2 in allLemma (sym p2) p

There's a section at the bottom of http://docs.idris-lang.org/en/latest/tutorial/views.html explaining this, basically fx is the name of the variable that will hold the proof that the expression being matched on equals the corresponding result for each matcher branch.

Oh my god, this is incredible! It's like Idris has the "inspect" pattern from Agda built right in! Thanks for showing me