A Question about Magic With --- Resolved

While I was on the bed listening to Eric Clapton's Bell Bottom Blues, it occurred to me that I could probably use subst to replace partition p xs with < ys , zs >, i.e., something like

subst (\X -> EqualLength xs (pair-concat X))
      (refl {< ys , zs >}) (partition xs p)

I expect there are some mysterious connection between a term and a pattern that is matched with the term, which would remind Agda that partition p xs is in fact < ys , zs >. Unfortunately it failed. But not much later I came up with the idea that maybe doing a direct with-match on partition-lenpres xs p would work, and indeed it worked! The final result is

partition-lenpres : (xs : List Nat)(p : Nat) ->
                      EqualLength xs (pair-concat (partition p xs))
partition-lenpres [] _ = eqlen-base
partition-lenpres (x :: xs) p with partition p xs | cmp x p
                                 | partition-lenpres xs p  -- magic with
... | < ys , zs > | \/-IL x≼p | indHyp = eqlen-step indHyp
... | < ys , zs > | \/-IR p≼x | indHyp = lemma1 x x xs ys zs indHyp

where lemma1 has been proved when I was working on the "intrusive" proof.

lemma1 : {A : Set}(x z : A)(xs ys zs : List A) ->
          EqualLength xs (ys ++ zs) -> EqualLength (x :: xs) (ys ++ z :: zs)

--
Excellent! Though I still don't understand exactly how with works...