≡-Рассуждение и "с" образцами

Я доказал некоторые свойства filter и map, все прошло неплохо, пока я не наткнулся на это свойство: filter p (map f xs) ≡ map f (filter (p ∘ f) xs). Вот часть кода, которая имеет значение:

open import Relation.Binary.PropositionalEquality
open import Data.Bool
open import Data.List hiding (filter)

import Level

filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
filter _ [] = []
filter p (x ∷ xs) with p x
... | true  = x ∷ filter p xs
... | false = filter p xs

Теперь, поскольку я люблю писать доказательства, используя модуль ≡-Reasoning, первое, что я пробовал, было:

open ≡-Reasoning
open import Function

filter-map : ∀ {a b} {A : Set a} {B : Set b}
             (xs : List A) (f : A → B) (p : B → Bool) →
             filter p (map f xs) ≡ map f (filter (p ∘ f) xs)
filter-map []       _ _ = refl
filter-map (x ∷ xs) f p with p (f x)
... | true = begin
  filter p (map f (x ∷ xs))
    ≡⟨ refl ⟩
  f x ∷ filter p (map f xs)
--  ...

Но, увы, это не сработало. Пробыв в течение часа, я, наконец, сдался и доказал это следующим образом:

filter-map (x ∷ xs) f p with p (f x)
... | true  = cong (λ a → f x ∷ a) (filter-map xs f p)
... | false = filter-map xs f p

По-прежнему интересно, почему переход через ≡-Reasoning не работал, я пробовал что-то очень тривиальное:

filter-map-def : ∀ {a b} {A : Set a} {B : Set b}
                 (x : A) xs (f : A → B) (p : B → Bool) → T (p (f x)) →
                 filter p (map f (x ∷ xs)) ≡ f x ∷ filter p (map f xs)
filter-map-def x xs f p _  with p (f x)
filter-map-def x xs f p () | false
filter-map-def x xs f p _  | true = -- not writing refl on purpose
  begin
    filter p (map f (x ∷ xs))
  ≡⟨ refl ⟩
    f x ∷ filter p (map f xs)
  ∎

Но typechecker не согласен со мной. Казалось бы, что текущая цель остается filter p (f x ∷ map f xs) | p (f x), и хотя шаблон, сопоставляемый с p (f x), filter, просто не уменьшится до f x ∷ filter p (map f xs).

Есть ли способ сделать эту работу с ≡-Reasoning?

Спасибо!