α✝ : Type u_1
l r : RBNode α✝
p : α✝ → Prop
hl : All p l
hr : All p r
⊢ All p
    (match l, r with
    | nil, x => x
    | x, nil => x
    | node red a x b, node red c y d =>
      match append b c with
      | node red b' z c' => node red (node red a x b') z (node red c' y d)
      | bc => node red a x (node red bc y d)
    | node black a x b, node black c y d =>
      match append b c with
      | node red b' z c' => node red (node black a x b') z (node black c' y d)
      | bc => balLeft a x (node black bc y d)
    | a@h:(node black l v r), node red b x c => node red (append a b) x c
    | node red a x b, c@h:(node black l v r) => node red a x (append b c))
α✝ : Type u_1
l r : RBNode α✝
p : α✝ → Prop
hl : All p l
hr : All p r
⊢ All p (append l r)
unfold append
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))

case h_5
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ l✝ : RBNode α✝
v✝ : α✝
r✝ b✝ : RBNode α✝
x✝ : α✝
c✝ : RBNode α✝
hl : All p (node black l✝ v✝ r✝)
hr : All p (node red b✝ x✝ c✝)
⊢ p x✝ ∧ All p (append (node black l✝ v✝ r✝) b✝) ∧ All p c✝

case h_6
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node black l✝ v✝ r✝)
⊢ p x✝ ∧ All p a✝ ∧ All p (append b✝ (node black l✝ v✝ r✝))
α✝ : Type u_1
l r : RBNode α✝
p : α✝ → Prop
hl : All p l
hr : All p r
⊢ All p
    (match l, r with
    | nil, x => x
    | x, nil => x
    | node red a x b, node red c y d =>
      match append b c with
      | node red b' z c' => node red (node red a x b') z (node red c' y d)
      | bc => node red a x (node red bc y d)
    | node black a x b, node black c y d =>
      match append b c with
      | node red b' z c' => node red (node black a x b') z (node black c' y d)
      | bc => balLeft a x (node black bc y d)
    | a@h:(node black l v r), node red b x c => node red (append a b) x c
    | node red a x b, c@h:(node black l v r) => node red a x (append b c))
split <;> simp [*]
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
have ⟨hx, ha, hb⟩ := hl
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
have ⟨hy, hc, hd⟩ := hr
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (append b✝ c✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
have := hb.append hc
no goals
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (append b✝ c✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))
split <;> simp_all
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
have ⟨hx, ha, hb⟩ := hl
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
have ⟨hy, hc, hd⟩ := hr
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (append b✝ c✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
have := hb.append hc
no goals
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
this : All p (append b✝ c✝)
⊢ All p
    (match append b✝ c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => balLeft a✝ x✝ (node black bc y✝ d✝))
split <;> simp_all [All.balLeft]
no goals
case h_5
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ l✝ : RBNode α✝
v✝ : α✝
r✝ b✝ : RBNode α✝
x✝ : α✝
c✝ : RBNode α✝
hl : All p (node black l✝ v✝ r✝)
hr : All p (node red b✝ x✝ c✝)
⊢ p x✝ ∧ All p (append (node black l✝ v✝ r✝) b✝) ∧ All p c✝
simp_all [hl.append hr.2.1]
no goals
case h_6
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ l✝ : RBNode α✝
v✝ : α✝
r✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node black l✝ v✝ r✝)
⊢ p x✝ ∧ All p a✝ ∧ All p (append b✝ (node black l✝ v✝ r✝))
simp_all [hl.2.2.append hr]