open import Logic::False
open import Arith::Bool::Core

open data Dec (P : Type)
| yes P
| no (¬ P)

def forget {P : Type} (d : Dec P) : Bool
| yes _ ⇒ true
| no _ ⇒ false

def decide {P A : Type} (d : Dec P) (t f : A) : A ⇒ ifElse (forget d) t f

open data Tri (A B C : Type)
| yesA A
| yesB B
| yesC C