QSort in Agda, Round 3

After figuring out how to use the magic with, the rest is quite straightforward --- the logic is identical to the one used to prove the intrusive version.

qsort-lenpres : ∀ (\xs -> EqualLength xs (qsort xs))
qsort-lenpres [] = eqlen-base
qsort-lenpres (x :: xs) with partition x xs | partition-lenpres xs x
qsort-lenpres (x :: xs) | < ys , zs > | ind-hyp₁ with qsort-lenpres ys
                                                   | qsort-lenpres zs
qsort-lenpres (x :: xs) | < ys , zs > | ind-hyp₁ | ind-hyp₂ | ind-hyp₃ =
  chainˡ> x :: xs
     ===ˡ qsort ys ++ x :: qsort zs byˡ lemma1 x x xs (qsort ys) (qsort zs)
          (chainˡ> xs
              ===ˡ ys ++ zs byˡ ind-hyp₁
              ===ˡ qsort ys ++ qsort zs byˡ lemma2 ind-hyp₂ ind-hyp₃)

It seems that one has to with-match partition x xs and partition-lenpres xs x simultaneously in order to make Agda know that partition x xs is indeed < ys , zs > when it is inferring the type of ind-hyp₁.

--
I really have to go to bed now since I've got a midterm in the morning. XD