α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y 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 (balance1 l v r) ↔ p v ∧ All p l ∧ All p r
unfold balance1
no goals
α : Type u_1
p : α → Prop
l : RBNode α
v : α
r : RBNode α
⊢ All p
      (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y 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]