This can make use of the following things I've developed tonight:
unification for ABTs (only renamings of metavariables needed/supported at the moment)
alpha-respecting "subtelescope" relation
Then, suppose the goal is J. Then, if the new subgoals are a telescope T such that [x:J] <: T for some fresh metavariable x, then we have not made progress, and the tactical should fail.
Note: we can't just search the telescope for exactly J, since the metavariables/holes may have been renamed by the tactic.
This can make use of the following things I've developed tonight:
Then, suppose the goal is
J. Then, if the new subgoals are a telescopeTsuch that[x:J] <: Tfor some fresh metavariablex, then we have not made progress, and the tactical should fail.Note: we can't just search the telescope for exactly
J, since the metavariables/holes may have been renamed by the tactic.