Modernize the Coq strict positivity example

It's now possible to (unsoundly) disable the positivity check, so the example can use an otherwise-ordinary inductive definition rather than a set of axioms.