Not optimal derivation order for `AllLTE`

[DanMax03]

Consider the following example:

data VectNat : Nat -> Type where
  Nil : VectNat Z
  (::) : Nat -> VectNat n -> VectNat (S n)

data AllLTE : VectNat n -> VectNat n -> Type where
  Base : AllLTE [] []
  Step : LTE x y =>
         AllLTE xs ys ->
         AllLTE (x :: xs) (y :: ys)

g : Fuel ->
    {n : _} -> (l1, l2 : VectNat n) ->
    Gen MaybeEmpty $ AllLTE l1 l2
g = deriveGen

Logging shows that Step is generated with not optimal order of its parameters. It would be much faster if it tried to generate LTE and only then went to the recursive path

[ build ] LOG deptycheck.derive.consBody:2: Spec.AllLTE[0(n), 1, 2] Step __ start __
[ build ] LOG deptycheck.derive.least-effort:15: Spec.AllLTE[0(n), 1, 2] Step - determ: {#0 -> <=[] ->[], #1 (ys) -> <=[] ->[#0], #2 (xs) -> <=[] ->[#0], #3 (y) -> <=[] ->[], #4 (x) -> <=[] ->[], #5 -> <=[] ->[#3 (y), #4 (x)], #6 -> <=[] ->[#0, #1 (ys), #2 (xs)]}
[ build ] LOG deptycheck.derive.least-effort:15: Spec.AllLTE[0(n), 1, 2] Step - givs: [#0, #1 (ys), #2 (xs), #3 (y), #4 (x)]
[ build ] LOG deptycheck.derive.least-effort:7: Spec.AllLTE[0(n), 1, 2] Step - used final order: [#6, #5]
[ build ] LOG deptycheck.derive.closuring.internal:20: Spec.AllLTE[0(n), 1, 2] is used as an internal generator
[ build ] LOG deptycheck.derive.closuring.internal:20: Data.Nat.LTE[0(n), 1(m)] is used as an internal generator
[ build ] LOG deptycheck.derive.consBody:2: Spec.AllLTE[0(n), 1, 2] Step ^^  end  ^^