no goals
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : decide p = decide q
⊢ p ↔ q
rw [← decide_eq_true_iff p, h, decide_eq_true_iff]
no goals
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p ↔ q
⊢ decide p = decide q
simp [h]