<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<p>I didn't try, but how about pattern match on y, for example in a
with-clause? Then the proof should be refl.<br>
</p>
<br>
<div class="moz-cite-prefix">On 2017-07-03 15:34, v0id_NULL wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAE3YR0Xf2M1hV8St1BcjyswNQrUSckfCnzd1cDu3sNbW26E5xQ@mail.gmail.com">
<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>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>