iApply: Add sufficiently many  spec patterns per default?
I find my self repeatedly writing
iApply (foo with "  ") in lambdaRust proofs. Would it make sense to extend the automatic "adding a
 to the end of th spec pattern list" that
iApply does, such that it will add as many
 as are needed to get the job done? Essentially,
iApply foo would always succeed if the conclusion of foo matches the goal, and all assumptions will only get the persistent contect -- spec patterns are only needed if one wants to give more than that? IMHO that would also improve the general workflow of working with
iApply since I don't need to look up in advance how many items I need to put into the spec pattern, I can just
iApply and then see which of the goals I get need further resources.