Agda: Erro de análise ao provar que ¬Any≃All¬

Estou tentando provar

¬Any≃All¬ : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (¬_ ∘ Any P) xs ≃ All (¬_ ∘ P) xs

Eu defini

to [] t = []
to (x :: xs) v = (v ∘ here) ∷ to xs (v ∘ there)

from [] [] ()
from (x :: xs´) (¬Px ∷ ¬Pxs´) = λ { (here Px) → ¬Px Px ; (there Pxs´) → (from xs´ ¬Pxs´) Pxs´}

O problema vem da tentativa de definir

FromTo : ∀ {A : Set} → {P : A → Set} → (xs : List A) → (v : (¬_ ∘ Any P) xs) → ((from xs) ∘ (to xs)) v ≡ v 

Minha ideia é escrever algo assim:

FromTo [] t = extensionality (λ {()})
FromTo (x :: xs´) v =
  begin
    ((from (x :: xs´)) ∘ (to (x :: xs´))) v 
  ≡⟨⟩
    (from (x :: xs´))(to (x :: xs´) v)
  ≡⟨⟩
    (from (x :: xs´))((v ∘ here) ∷ (to xs´ (v ∘ there)))
  ≡⟨⟩
    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩ -- PARSE ERROR
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨ FromTo xs´ (λ u → v (there u)) ⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (v ∘ there) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → v (there Pxs´) }
  ≡⟨⟩
    v
  ∎

O problema que tenho é que tenho um erro de análise estranho:

 Parse error
≡⟨⟩<ERROR>
        λ { (here Px´) → v (h...

localizado aqui:

    λ { (here Px´) → (v ∘ here) Px´ ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }
  ≡⟨⟩
    λ { (here Px´) → v (here Px´)  ; (there Pxs´) → (from xs´ (to xs´ (v ∘ there))) Pxs´ }

Tentei de tudo para ver se estava faltando algum espaço em branco ou se as tabulações estavam erradas ou o que quer que seja, mas nada. O problema aparece quando há duas lambdas separadas por um ≡⟨⟩.