module Data.List.Properties.Extra {a}{A : Set a} where

open import Data.Nat
open import Data.Fin hiding (_<_)
open import Data.List
open import Data.Product hiding (map)
open import Data.Fin using (fromℕ≤; zero; suc)
open import Data.List.All hiding (lookup; map)
open import Data.List.Any hiding (map)
open import Data.List.Any.Membership.Propositional

open import Relation.Binary.List.Pointwise hiding (refl; map)
open import Relation.Binary.PropositionalEquality

∈-∷ʳ : ∀ (l : List A)(x : A) → x ∈ (l ∷ʳ x)
∈-∷ʳ [] x = here refl
∈-∷ʳ (x ∷ l) y = there (∈-∷ʳ l y)

infixl  _[_]≔_
_[_]≔_ : (l : List A) → Fin (length l) → A → List A
[] [ () ]≔ x
(x ∷ xs) [ zero ]≔ x' = x' ∷ xs
(x ∷ xs) [ suc i ]≔ y = xs [ i ]≔ y

infixl  _[_]≔'_
_[_]≔'_ : ∀ {x} → (l : List A) → x ∈ l → A → List A
[] [ () ]≔' y
(x ∷ l) [ here px ]≔' y = y ∷ l
(x ∷ l) [ there px ]≔' y = x ∷ (l [ px ]≔' y)

≔'-[]= :  ∀ {x}{l : List A} (p : x ∈ l) → ∀ {y} → y ∈ (l [ p ]≔' y)
≔'-[]= (here px) = here refl
≔'-[]= (there p) = there (≔'-[]= p)

drop-prefix : ∀ (l m : List A) → drop (length l) (l ++ m) ≡ m
drop-prefix [] m = refl
drop-prefix (x ∷ l) m = drop-prefix l m