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