α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ toList t
α : Type u_1
x : α
t : Ordnode α
⊢ Emem x t ↔ x ∈ toList t
unfold Emem
no goals
α : Type u_1
x : α
t : Ordnode α
⊢ Any (Eq x) t ↔ x ∈ toList t
induction t <;> simp [Any, *, or_assoc]