no goals
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
⊢ decide p = decide q
cases h' : decide q with
| false => exact decide_false (mt h.1 <| of_decide_false h')
| true => exact decide_true (h.2 <| of_decide_true h')
no goals
case false
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = false
⊢ decide p = false
exact decide_false (mt h.1 <| of_decide_false h')
no goals
case true
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
h' : decide q = true
⊢ decide p = true
exact decide_true (h.2 <| of_decide_true h')