はB`がすでに

Question

に一致したとき、 `私は、単純な何かを証明しようとしています` TのB`を証明：

open import Data.List 
open import Data.Nat 
open import Data.Bool 
open import Data.Bool.Properties 
open import Relation.Binary.PropositionalEquality 
open import Data.Unit 

repeat : ∀ {a} {A : Set a} → ℕ → A → List A 
repeat zero x = [] 
repeat (suc n) x = x ∷ repeat n x 

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n → 
    filter p (repeat n x) ≡ repeat n x 

私はfilter-repeatを証明するp xにパターンマッチングによって簡単になるだろうと思った：

filter-repeat p x prf zero = refl 
filter-repeat p x prf (suc n) with p x 
filter-repeat p x() (suc n) | false 
filter-repeat p x prf (suc n) | true = cong (_∷_ x) (filter-repeat p x prf n) 

しかし、これはprf : ⊤がタイプT (p x)ではないと訴えています。だから私は、OK、これはおなじみの問題のように思える、と思ったのは、inspectをサッと取り出してみましょう：

filter-repeat p x prf zero = refl 
filter-repeat p x prf (suc n) with p x | inspect p x 
filter-repeat p x() (suc n) | false | _ 
filter-repeat p x tt (suc n) | true | [ eq ] rewrite eq = cong (_∷_ x) (filter-repeat p x {!!} n) 

しかしrewriteにもかかわらず、穴のタイプは、まだT (p x)の代わりT trueです。何故ですか？タイプをT trueに減らすにはどうすればいいですか？ttと記入できますか？

回避策は、私がT-≡を使用して、それを回避することができました：

open import Function.Equality using (_⟨$⟩_) 
open import Function.Equivalence 

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n → 
    filter p (repeat n x) ≡ repeat n x 
filter-repeat p x prf zero = refl 
filter-repeat p x prf (suc n) with p x | inspect p x 
filter-repeat p x() (suc n) | false | _ 
filter-repeat p x tt (suc n) | true | [ eq ] = cong (_∷_ x) (filter-repeat p x (Equivalence.from T-≡ ⟨$⟩ eq) n) 

が、私はまだinspectベースのソリューションが動作しない理由を理解したいと思います。