α : Type u_1
cut : α → Ordering
t' : RBNode α
p' : Path α
t : RBNode α
eq : zoom cut t root = (t', p')
⊢ toList (fill root t) = toList t
α : Type u_1
cut : α → Ordering
t' : RBNode α
p' : Path α
t : RBNode α
eq : zoom cut t root = (t', p')
⊢ withList p' (toList t') = toList t
rw [← fill_toList, ← zoom_fill eq]
no goals
α : Type u_1
cut : α → Ordering
t' : RBNode α
p' : Path α
t : RBNode α
eq : zoom cut t root = (t', p')
⊢ toList (fill root t) = toList t
rfl