This way we can use uPred_valid for validity of uPreds, which
more sense.

As proposed by JH Jourdan in issue 34.

We only had the step-indexed version before. Unfortunately, the non
step-indexed version does not follow from the step-indexed version.

This also solves a name clash with the extension order of CMRAs.

Before, it failed when these tactics were invoked with persistent
hypotheses. The new behavior is more convenient when using these
tactics to build other tactics.

This comment mostly addresses issue #34.

There are still some issues:

- For iLöb we can write `iLöb (x1 .. xn) as "IH"` to revert x1 .. xn
  before performing Löb induction. An analogue notation for iInduction
  results in parsing conflicts.
- The names of the induction hypotheses in the Coq intro pattern are
  ignored. Instead, when using `iInduction x as pat "IH"` the induction
  hypotheses are given fresh names starting with "IH". The problem here
  is that the names in the introduction pattern are idents, whereas the
  induction hypotheses are inserted into the proof mode context, and thus
  need to have strings as names.

This closes issue 32.

This solves issue 33.

Make the elements of gset persistent by changing the core



See merge request !11

This makes the typeclass mechanism able to use instances like [Is_true X -> Blah], where X reduces to X.