In some cases, a lemma we generate would verify faster if one removed preconditions from it. For instance, if one of the preconditions involves a loosely-triggered quantifier, it might be useful to remove it. So, it may be useful to allow a recipe to specify a lemma customization that, rather than adding material to the body of the proof, instead removes certain specified preconditions.
This issue is a generalization of issue #5, so its solution may also fix that issue.
In some cases, a lemma we generate would verify faster if one removed preconditions from it. For instance, if one of the preconditions involves a loosely-triggered quantifier, it might be useful to remove it. So, it may be useful to allow a recipe to specify a lemma customization that, rather than adding material to the body of the proof, instead removes certain specified preconditions.
This issue is a generalization of issue #5, so its solution may also fix that issue.