pf-redreddepth : (t : Tree) -> {pf : T (is-just (redRed t))} -> (depth t ≡ depth (proj₁ (to-witness-T (redRed t) pf)))
pf-redreddepth (Red Leaf (Red rl rr _) _) = refl
pf-redreddepth (Red (Red ll lr _) r _) = refl
pf-redreddepth (Red l@(Black _ _ _) (Red _ _ _) _) = refl

pf-depthbalance :
       (l : Tree)
    -> (r : Tree)
    -> (k : ℕ)
    -> (1 + depth l ≡ depth (balance l r k))
pf-depthbalance l r k with redRed l
pf-depthbalance l r k | pf@(just (ll₁ , i , ll₂ , j , ll₃)) = cong suc $ pf-redreddepth l
pf-depthbalance l r k | nothing = {!!}