α : Sort u_1
β : Sort ?u.36335
σ : α → Sort ?u.36331
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b
α : Sort u_1
β : Sort ?u.36335
σ : α → Sort ?u.36331
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ (fun x => b) h) ↔ ¬P ∧ a ≠ b
simp only
no goals
α : Sort u_1
β : Sort ?u.36335
σ : α → Sort ?u.36331
f : α → β
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
a b c : α
A : P → α
B : ¬P → α
⊢ (∃ h, a ≠ b) ↔ ¬P ∧ a ≠ b
rw [exists_prop]