Foo.idr

module Foo

data Singleton : (x : k) -> Type where
  With : (y : a) -> x = y -> Singleton x

inspect : (x : a) -> Singleton x
inspect x = With x Refl

all_values_filtered : (xs:List a) -> (f:a -> Bool) -> (all f (filter f xs) = True)
all_values_filtered [] f = Refl
all_values_filtered (x :: xs) f with (inspect (f x))
  all_values_filtered (x :: xs) f | (With False prf) =
    rewrite prf in all_values_filtered xs f
  all_values_filtered (x :: xs) f | (With True prf) =
       rewrite prf
    in rewrite prf
    in rewrite all_values_filtered xs f
    in Refl


--