no goals
α : Type u_1
P : α → Prop
⊢ ∀ (x : α), Emem x nil → P x
rintro _ ⟨⟩
no goals
α : Type u_1
P : α → Prop
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ All P (node size✝ l x r) ↔ ∀ (x_1 : α), Emem x_1 (node size✝ l x r) → P x_1
simp [All, Emem, all_iff_forall, Any, or_imp, forall_and]