omega: Handles two-element Prod.Lex, but not three elements

[nomeata]

@hargoniX and I just ran into this while proving termination with a rather complex termination measure: omega has some support for Lex.Prod, but breaks when nesting it:

example : Prod.Lex (· < ·) (· < ·) (0, 0) (0, 1) :=
  by omega -- works

example : Prod.Lex (· < ·) (Prod.Lex (· < ·) (· < ·)) (0, 0, 0) (0, 1, 0) :=
  by omega -- fails

Versions

0.4.7

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[Kha]

We're not planning to further increase the scope of omega but to embed it into more general tactics instead