<div dir="ltr"><div><div>Cool, thanks!<br></div>I will go this way.<br><br></div>Cheers,<br>Dmytro <br><br></div><div class="gmail_extra"><br><div class="gmail_quote">2014-12-06 21:52 GMT+02:00 flicky frans <span dir="ltr"><<a href="mailto:flickyfrans@gmail.com" target="_blank">flickyfrans@gmail.com</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Here is one another option:<br>
<br>
open import Data.Bool<br>
open import Relation.Binary.PropositionalEquality<br>
<span class=""><br>
data Term : Bool → Set where<br>
I : Term false<br>
App : (a b : Bool) → Term a → Term b → Term (a ∨ b)<br>
<br>
</span>test' : ∀ {a} → a ≡ false → Term a → Set<br>
test' p I = Bool<br>
test' p (App false false t1 t2) = Bool<br>
test' () (App false true t1 t2)<br>
test' () (App true b t1 t2)<br>
<br>
test : Term false → Set<br>
test = test' refl<br>
<div class="HOEnZb"><div class="h5">_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>