iSpecialize should work even if the wand is under a later.
In the proofmode, if I have, say, the hypothesis "H1" : ▷ (A -* B)
, then iSpecialize ("H1" with "[]")
does not work. Is there any good reason for this ?
In the proofmode, if I have, say, the hypothesis "H1" : ▷ (A -* B)
, then iSpecialize ("H1" with "[]")
does not work. Is there any good reason for this ?