module Test
import Data.Vect


removeFalses : Vect n Bool -> (m ** Vect m Bool)
removeFalses [] = (Z ** [])
removeFalses (True :: xs) = let (m ** xs') = removeFalses xs in (S m ** True :: xs')
removeFalses (False :: xs) = removeFalses xs


f : (xs : Vect (S n) Bool) -> Elem True xs -> (Bool, Bool)
f elems p with (removeFalses elems) proof w
    | (Z ** []) = ?help1
    | (S m ** x :: xs) = let Refl = w in ?help2