dsf.idr

bool' : Bool -> a -> a -> a
bool' True x _ = x
bool' False _ y = y
  
filter' : (a -> Bool) -> List a -> List a
filter' f [] = []
filter' f (x :: xs) = bool' (f x) (x :: filter' f xs) (filter' f xs)

an : Bool -> Bool -> Bool
an True True = True
an _ _ = False

all' : (a -> Bool) -> List a -> Bool
all' f [] = True
all' f (x :: xs) = an (f x) (all' f xs)

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 (f x)
  all_values_filtered (x :: xs) f | False = all_values_filtered xs f
  all_values_filtered (x :: xs) f | True = ?already_forgot_that_f_x_is_True

{-
  a : Type
  x : a
  xs : List a
  f : a -> Bool
--------------------------------------
already_forgot_that_f_x_is_True : an (f x) (all' f (filter' f xs)) = True
-}