Give a canonical ordering for destructing terms in Wingman

[isovector]

Today, Wingman tries to destruct terms in any order. For example, when trying to synthesize zip, it will try the following solutions:

\ l_a l_b
  -> case l_b of
       []
         -> case l_a of
              [] -> _
              (a : l_a3) -> _
       (b : l_b3)
         -> case l_a of
              [] -> _
              (a : l_a5) -> _

and

\ l_a l_b
  -> case l_a of
       []
         -> case l_b of
              [] -> _
              (b : l_b3) -> _
       (a : l_a3)
         -> case l_b of
              [] -> _
              (b : l_b5) -> _

These two solutions are equal modulo the order in which we did a pattern match. But it's stupid to explore both paths, since they cannot produce different answers.

Instead, this PR introduces a canonical ordering on the destructing on terms, using the natural ordering of introduction in the hypothesis. In particular, Wingman will not try to destruct anything that was introduced before something that has already been destructed.

This change has a remarkable O(n!) asymptotic increase at each hole 🤩 The search is still remains stupid, but at least it's no longer factorially stupid.