gistfile1.agda

  _∉_ : ∀ {n m} {A : Set n} → A → Vec A m → Set n
  a ∉ v = ¬ (a ∈ v)
  
  postulate take' : ∀ {n m} {A : Set n} → (i : Fin m) → Vec A m → Vec A (toℕ i)
  -- take' i v = ?

  postulate indexof : ∀ {n m a} {A : Set n}
                      → (v : Vec A m) → (p : A → Set) 
                      → Dec (∃ λ i → p (lookup i v) × a ∉ (take' i v))
 
-- Cannot instantiate the metavariable _70 to solution A since it
-- contains the variable A which is not in scope of the metavariable
-- or irrelevant in the metavariable but relevant in the solution
-- when checking that the expression take' i v has type
-- Vec _70 (_m_86 v p i)