Agda-Edit-Time-tactics

open import Data.List
import Data.List.Any as LAny
open import Relation.Binary  as B
open import Relation.Binary.PropositionalEquality

open import Data.Nat

_∈_ : ∀ {a} {A : Set a} → A → List A → Set a
a ∈ as = LAny.Any (a ≡_) as

indexOf∈ : ∀ {a} {A : Set a}
       → {xs : List A}
       → {x : A}
       → x ∈ xs
       → ℕ
indexOf∈ (LAny.here px) = zero
indexOf∈ (LAny.there p) = suc (indexOf∈ p)


om6-Lemma3 : ∀ {a b} {A : Set a} {B : Set b}
         → {n : ℕ}
         → {xs : List A}
         → {ys : List A}
         → {x : B}
         → length xs ≡ n
         → (f : A → B)
         → (p : x ∈ map f (xs ++ ys))
         → indexOf∈ p < n
         → x ∈ map f xs
om6-Lemma3 = λ z f → λ { () }
{-
  om6-Lemma3 {xs = []} {ys} refl f p ()
  om6-Lemma3 {xs = x ∷ xs} {ys} refl f (here px) (s≤s i<) = here px
  om6-Lemma3 {xs = x ∷ xs} {ys} refl f (there p) (s≤s i<) = there (om6-Lemma3 refl f p i<)
-}