cases b
b : Bool
h : Decidable (b = true)
⊢ decide (b = true) = b
case false
h : Decidable (false = true)
⊢ decide (false = true) = false

case true
h : Decidable (true = true)
⊢ decide (true = true) = true