α : Type u_1
p : α → Prop
t : RBNode α
h : All p t
⊢ All p
    (match t with
    | node c a v b => node red a v b
    | nil => nil)
α : Type u_1
p : α → Prop
t : RBNode α
h : All p t
⊢ All p (setRed t)
unfold setRed
no goals
α : Type u_1
p : α → Prop
t : RBNode α
h : All p t
⊢ All p
    (match t with
    | node c a v b => node red a v b
    | nil => nil)
split <;> simp_all