no goals
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (node4R l x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r
cases m <;> simp [node4R, all_node', All, all_node3R, and_assoc]