[Agda] Some proofs by clauses

[v0id_NULL]

Dear list,

Help me please. How can I prove type of p2?

module M1 where

open import Data.Nat using (ℕ)
open import Data.Bool using (Bool; true; false)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

f : Bool → Bool → ℕ
f true x = 1
f y false = 2
f false true = 3

p1 : {x : Bool} → f true x ≡ 1
p1 = refl

p2 : {y : Bool} → f y false ≡ 2
p2 = {!!}

p3 : f false true ≡ 3
p3 = refl
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170703/c93cc4c9/attachment.html>