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.