open import Arith::Bool::Core using (Bool, true, false)
open import Logic::False      using (¬)
open import Logic::Dec

open data Reflect Type Bool
| P, true  ⇒ reflectT P
| P, false ⇒ reflectF (¬ P)

def downgrade {P : Type} {b : Bool} (Reflect P b) : Dec P
| reflectT proof ⇒ yes proof
| reflectF proof ⇒ no proof