<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">&lt;<a href="mailto:flickyfrans@gmail.com" target="_blank">flickyfrans@gmail.com</a>&gt;</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&#39; : ∀ {a} → a ≡ false → Term a → Set<br>
test&#39; p   I                      = Bool<br>
test&#39; p  (App false false t1 t2) = Bool<br>
test&#39; () (App false true  t1 t2)<br>
test&#39; () (App true  b     t1 t2)<br>
<br>
test : Term false → Set<br>
test = test&#39; 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>