1
module EtaContractToMillerPattern where
3
data _==_ {A : Set}(a : A) : A -> Set where
6
record Prod (A B : Set) : Set where
14
test : let X : (Prod A B -> C) -> (Prod A B -> C)
16
in (x : Prod A B -> C) ->
17
X (\ z -> x (fst z , snd z)) == x
b'\\ No newline at end of file'