- GREAT: when unifying ?1 : Type[i] with ?2: Type[j] the unifier

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.