The status of Well-founded is unclear.

Today, it is used for Int, which is not right, because integers are not well-founded. But this is more-or less sound because Why3 adds the requirement that the variant need to be positive.

We need to do something close to Why3, an allow variants in the following cases:

• The type is well-founded. In the case, tell Why3 that we are using our specific order relation (I don't think we are doing that right now, do we?)
• The type is Int, and let Why3 add the requirement that the variant needs to be positive
• The type is algebraic, and not marked as well-founded. Do as in Why3: do structural recursion.
• Tuples with lexicographic ordering of the previous cases? Is this even possible to tell Why3 to use different kinds of orderings on different elements of the tuple?