α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp
      (match t with
      | nil => nil
      | node c l v r => node black l v r) ↔
    Ordered cmp t
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp (setBlack t) ↔ Ordered cmp t
unfold setBlack
no goals
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp
      (match t with
      | nil => nil
      | node c l v r => node black l v r) ↔
    Ordered cmp t
split <;> simp [Ordered]