α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
      | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b) ↔
    p v ∧ All p l ∧ All p r
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p (balance2 l v r) ↔ p v ∧ All p l ∧ All p r
unfold balance2
no goals
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | a, x, node red (node red b y c) z d => node red (node black a x b) y (node black c z d)
      | a, x, node red b y (node red c z d) => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b) ↔
    p v ∧ All p l ∧ All p r
split <;> simp [and_assoc, and_left_comm]