[Agda] proofs and case-split

[Andreas Buechele]

Hello,

I'm trying to proof some properties on AVL trees from the standard
library: If a property P holds for all tree elements, it holds also for
all tree elements after calling joinˡ⁺.

---8<---
open import Data.Unit

HoldsAll : {n : ℕ} -> (KV -> Set) -> Tree n -> Set
HoldsAll P leaf = ⊤
HoldsAll P (node l k r _) = P k × (HoldsAll P l) × (HoldsAll P r)

join1+HoldsAll :  ∀ {hˡ hʳ} -> {P : KV -> Set}
                  -> (left : (∃ λ i -> Tree (i ⊕ hˡ)))
                  -> (value : KV)
                  -> (right : Tree hʳ)
                  -> (bal : hˡ ∼ hʳ)
                  -> HoldsAll P (proj₂ left)
                  -> P value
                  -> HoldsAll P right
                  -> HoldsAll P (proj₂ (joinˡ⁺ left value right bal))
join1+HoldsAll (1# , node t₁ k₂ (node t₃ k₄ t₅ bal) ∼+) k₆ t₇ ∼- hl hv
hr = {!!}
join1+HoldsAll (1# , node t₁ k₂ t₃ ∼-) k₄ t₅ ∼- hl hv hr = {!!}
join1+HoldsAll (1# , node t₁ k₂ t₃ ∼0) k₄ t₅ ∼- hl hv hr = {!!}
join1+HoldsAll (1# , t₁) k₂ t₃ ∼0 hl hv hr = {!!}
join1+HoldsAll (1# , t₁) k₂ t₃ ∼+ hl hv hr = {!!}
join1+HoldsAll (0# , t₁) k₂ t₃ bal hl hv hr = hv , (hl , hr)
--->8---

I'm confused about the goals, except the last case.
For example the goal for the case next to last is

HoldsAll .P (proj₂ (joinˡ⁺ (1# , t₁) k₂ t₃ ∼+))

but I think it should be

Σ (.P k₂) (λ _ → Σ (HoldsAll .P t₁) (λ _ → HoldsAll .P t₃))

Why is that? Is there a smart solution for this problem?

Kind regards,
  Andreas