En AgdaIntro, la sección de vista explica:

..esecon no recuerda la conexión entre el término temporal y los patrones.

Eso significa cuando define

data   False : Set where
record True  : Set where

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False

infixr 30 _:all:_
data All {A : Set}(P : A -> Set) : List A -> Set where
  all[]   : All P []
  _:all:_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs) 

satisfies : {A : Set} -> (A -> Bool) -> A -> Set
satisfies p x = isTrue (p x)

data Find {A : Set}(p : A -> Bool) : List A -> Set where
  found : (xs : List A)(y : A) -> satisfies p y -> (ys : List A) -> 
           Find p (xs ++ y :: ys)
  not-found : forall {xs} -> All (satisfies (not � p)) xs -> 
              Find p xs

Y quieres probar

find1 :{A:Set}(p:A->Bool)(xs:ListA)->Find p xs 
find1 p [] = not-found all []
find1 p(x::xs) with p x
...| true  = found [] x {!!} xs
...| false = {!!}

El tipo de agujero ({!!}) Es Verdadero (p x), aunque ya coincidimos con p x y descubrimos que era cierto.

¡El compilador no es consciente de que hicimos una coincidencia de patrones en p x y nos pide una prueba de que p x es cierto!

Esto motiva la introducción de un nuevo tipo, el

..tipo de elementos de un tipo A junto con pruebas de que son iguales a alguna x dada en A.

data Inspect {A : Set}(x : A) : Set where
  it : (y : A) -> x == y -> Inspect x

inspect : {A : Set}(x : A) -> Inspect x
inspect x = it x refl

Con este tipo, la función find se puede escribir:

trueIsTrue : {x : Bool} -> x == true -> isTrue x
trueIsTrue refl = _

falseIsFalse : {x : Bool} -> x == false -> isFalse x
falseIsFalse refl = _

find : {A : Set}(p : A -> Bool)(xs : List A) -> Find p xs
find p [] = not-found all[]
find p (x :: xs) with inspect (p x)
... | it true prf = found [] x (trueIsTrue prf) xs
... | it false prf with find p xs
find p (x :: ._) | it false _   | found xs y py ys =
  found (x :: xs) y py ys
find p (x :: xs) | it false prf | not-found npxs =
  not-found (falseIsFalse prf :all: npxs)

AHORA, si quiero probar la siguiente propiedad:

predicate : ∀ {A : Set} {p : A -> Bool } {xs : List A } -> 
            All (satisfies' p) (filter p xs)

Tendré el mismo problema que con find, así que necesito una coincidencia de patrón en la inspección para obtener un testigo, pero yoADEMÁS necesita tener el compilador para progresar en el filtro en el casop x == true !

Si hago una coincidencia de patrones paralelos, el compilador los trata como expresiones independientes

predicate {A} {p} {xs = []} = all[]
predicate {A} {p} {xs = x :: xs} with p x
predicate {A} {p} {x :: xs} | px with  inspect (p x) 
predicate {A} {p} {x :: xs} | true | it true pf = {!!}
predicate {A} {p} {x :: xs} | true | it false pf = {!!} 
predicate {A} {p} {x :: xs} | false | it true pf = {!!}
predicate {A} {p} {x :: xs} | false | it false pf = {!!}

¿Cómo puedo decirle al compilador que las dos ramas están vinculadas de alguna manera? ¿Debo agregar una prueba de ello?