feat: inext with later credits

[alvinylt]

Description

Implements the tactic inext n credit: H.

Addresses #239.

Similar to the Rocq implementation, once all credits are consumed (that is, H becomes £ 0), the hypothesis is discarded.

The type class AddModal and its instances have already been ported in PR #470, but are nonetheless also included in this PR so that we can use them for this tactic.

This tactic is unique in the sense that it is relevant only for IProp GF where InvGS GF holds. Within the ProofModeM.runTactic block, we have the generic BI instance prop. Otherwise, if we use isDefEq to unify prop and InvGS GF manually, we still run into universal level problems:

Application type mismatch: The argument
  «$GF»
has type
  BundledGFunctors.{u✝, u✝, u✝}
of sort `Type (u✝ + 1)` but is expected to have type
  BundledGFunctors.{0, 0, 0}
of sort `Type 1` in the application ...

In the implementation, we use mkAppM so that the instance InvGS GF is synthesised automatically. Resolved in commits 9056733 and 9b1963a.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[alvinylt]

The latest improvement is to use the same trick for HeapLang tactics for matching IProp GF with prop, so that we can use Qq for building proofs in subsequent steps instead of inelegantly using mkApp.

Commits: 9056733 and 9b1963a