[ new ] first jab at a generalised IMLL + lollipop

* This is what adding lollipop to IMLL might look like. A strictly
  decreasing measure should make it "rather simple" to write a
  proven terminating algorithm.

* Whenever the prover uses a variable, it may create side conditions
  that one has to discharge. The intuition behind this approach is
  to have something akin to the spines exposed by neutral terms.