no goals
α : Sort u_1
β : Sort ?u.35831
σ : α → Sort ?u.35827
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (dite P A fun x => b) ≠ b ↔ ∃ h, A h ≠ b
simp only [Ne.def, dite_eq_right_iff, not_forall]