simp only [decide_eq_true_eq]
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), decide (p a) = true → decide (p b) = true → a = b
α : Type u
β : Type v
inst✝³ : BishopFin α
inst✝² : BishopFin β
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
p_unique : ∀ (a b : α), p a → p b → a = b
⊢ ∀ (a b : α), p a → p b → a = b