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

case true
h : Decidable (true = true)
⊢ decide (true = true) = true
b : Bool
h : Decidable (b = true)
⊢ decide (b = true) = b
cases b
no goals
case false
h : Decidable (false = true)
⊢ decide (false = true) = false
exact decide_eq_false $ λ j => by cases j
no goals
h : Decidable (false = true)
j : false = true
⊢ False
cases j
no goals
case true
h : Decidable (true = true)
⊢ decide (true = true) = true
exact decide_eq_true $ rfl