α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
⊢ All p
    (match cut a✝¹ with
    | Ordering.lt =>
      match isBlack a✝² with
      | black => balLeft (del cut a✝²) a✝¹ a✝
      | red => node red (del cut a✝²) a✝¹ a✝
    | Ordering.gt =>
      match isBlack a✝ with
      | black => balRight a✝² a✝¹ (del cut a✝)
      | red => node red a✝² a✝¹ (del cut a✝)
    | Ordering.eq => append a✝² a✝)
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
⊢ All p (del cut (node c✝ a✝² a✝¹ a✝))
unfold del
case h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.lt
⊢ All p
    (match isBlack a✝² with
    | black => balLeft (del cut a✝²) a✝¹ a✝
    | red => node red (del cut a✝²) a✝¹ a✝)

case h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.gt
⊢ All p
    (match isBlack a✝ with
    | black => balRight a✝² a✝¹ (del cut a✝)
    | red => node red a✝² a✝¹ (del cut a✝))

case h_3
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.eq
⊢ All p (append a✝² a✝)
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
⊢ All p
    (match cut a✝¹ with
    | Ordering.lt =>
      match isBlack a✝² with
      | black => balLeft (del cut a✝²) a✝¹ a✝
      | red => node red (del cut a✝²) a✝¹ a✝
    | Ordering.gt =>
      match isBlack a✝ with
      | black => balRight a✝² a✝¹ (del cut a✝)
      | red => node red a✝² a✝¹ (del cut a✝)
    | Ordering.eq => append a✝² a✝)
split
case h_1.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : isBlack a✝² = black
⊢ All p (balLeft (del cut a✝²) a✝¹ a✝)

case h_1.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : isBlack a✝² = red
⊢ All p (node red (del cut a✝²) a✝¹ a✝)
case h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.lt
⊢ All p
    (match isBlack a✝² with
    | black => balLeft (del cut a✝²) a✝¹ a✝
    | red => node red (del cut a✝²) a✝¹ a✝)
split
no goals
case h_1.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : isBlack a✝² = black
⊢ All p (balLeft (del cut a✝²) a✝¹ a✝)
exact ha.del.balLeft hy hb
no goals
case h_1.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.lt
x✝ : RBColor
heq✝ : isBlack a✝² = red
⊢ All p (node red (del cut a✝²) a✝¹ a✝)
exact ⟨hy, ha.del, hb⟩
case h_2.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : isBlack a✝ = black
⊢ All p (balRight a✝² a✝¹ (del cut a✝))

case h_2.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : isBlack a✝ = red
⊢ All p (node red a✝² a✝¹ (del cut a✝))
case h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.gt
⊢ All p
    (match isBlack a✝ with
    | black => balRight a✝² a✝¹ (del cut a✝)
    | red => node red a✝² a✝¹ (del cut a✝))
split
no goals
case h_2.h_1
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : isBlack a✝ = black
⊢ All p (balRight a✝² a✝¹ (del cut a✝))
exact ha.balRight hy hb.del
no goals
case h_2.h_2
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝¹ : Ordering
heq✝¹ : cut a✝¹ = Ordering.gt
x✝ : RBColor
heq✝ : isBlack a✝ = red
⊢ All p (node red a✝² a✝¹ (del cut a✝))
exact ⟨hy, ha, hb.del⟩
no goals
case h_3
α : Type u_1
p : α → Prop
cut : α → Ordering
c✝ : RBColor
a✝² : RBNode α
a✝¹ : α
a✝ : RBNode α
hy : p a✝¹
ha : All p a✝²
hb : All p a✝
x✝ : Ordering
heq✝ : cut a✝¹ = Ordering.eq
⊢ All p (append a✝² a✝)
exact ha.append hb