<div dir="ltr"><div style="font-size:12.8px">Dear list,</div><div style="font-size:12.8px"><br></div><div style="font-size:12.8px">Help me please. How can I prove type of p2?</div><div style="font-size:12.8px"><br></div><div><div><span style="font-size:12.8px">module M1 where</span></div><div><span style="font-size:12.8px"><br></span></div><div><div><span style="font-size:12.8px">open import Data.Nat using (ℕ)</span></div><div><span style="font-size:12.8px">open import Data.Bool using (Bool; true; false)</span></div><div><span style="font-size:12.8px">open import Relation.Binary.PropositionalEquality using (_≡_; refl)</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">f : Bool → Bool → ℕ</span></div><div><span style="font-size:12.8px">f true x = 1</span></div><div><span style="font-size:12.8px">f y false = 2</span></div><div><span style="font-size:12.8px">f false true = 3</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">p1 : {x : Bool} → f true x ≡ 1</span></div><div><span style="font-size:12.8px">p1 = refl</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">p2 : {y : Bool} → f y false ≡ 2</span></div><div><span style="font-size:12.8px">p2 = {!!}</span></div><div><span style="font-size:12.8px"><br></span></div><div><span style="font-size:12.8px">p3 : f false true ≡ 3</span></div><div><span style="font-size:12.8px">p3 = refl</span></div></div></div><div><br></div></div>