module Main

import Data.Vect
import Data.Fin

%default total

find : Eq x => List x -> x -> Maybe Int
find [] elem = Nothing
find (y :: xs) elem = if y == elem then (Just 0) else (map (\ n => n + 1) (find xs elem))

find2 : Eq x => {n : Nat} -> Vect n x -> x -> Maybe (Fin n)
find2 [] elem = Nothing
find2 (y :: xs) elem = if y == elem then (Just FZ) else (map FS (find2 xs elem))

ex : find2 [1, 2, 3] 2 = Just 1
ex = Refl

nothingProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> Not (Elem e v) -> (find2 v e) = Nothing
nothingProof n v elem notIn = ?noIdea1

justProof : Eq x => (n : Nat) -> (v : Vect n x) -> (e : x) -> (find2 v e = Just r) -> (index r v == e) = True
justProof n v elem findProof = ?noIdea2