ADT Plugin should auto-generate well-foundedness axioms for the generated types

[marcoeilers]

Possibly conditionally when the termination plugin is active as well.

Currently, the user has to manually write such axioms; otherwise, there is no way to e.g. prove the following function on lists well-founded:

function len(l: List[Val]): Int
  ensures result >= 0
  // decreases l
{
  l.isNil ? 0 : 1 + len(l.tail)
}