no goals
α : Type u_1
P : α → Prop
⊢ Any P nil → ∃ x, Emem x nil ∧ P x
rintro ⟨⟩
no goals
α : Type u_1
P : α → Prop
⊢ (∃ x, Emem x nil ∧ P x) → Any P nil
rintro ⟨_, ⟨⟩, _⟩
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Emem x_1 (node size✝ l x r) ∧ P x_1
simp only [Emem]
no goals
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ Any P (node size✝ l x r) ↔ ∃ x_1, Any (Eq x_1) (node size✝ l x r) ∧ P x_1
simp [Any, any_iff_exists, or_and_right, exists_or]