What is a good name for the premise in the rule for implication introduction?

Question

I have the following standard inference rule:

Rule (ImplicationIntroduction)
  Premise
    [P]...Q
  Conclusion
    P=>Q

I'm putting together the BNF to parse this and I have:

 metastatement                ::=   subproof

                                |   metavariable

                                ;



 subproof                     ::=   supposition "..." metastatement ;

 supposition                  ::=   "[" metastatement "]" ;

The metaVariable rule is given elsewhere, by the way, in the BNF that puts this snippet in context.

Here I've copied Stanford and called the premise subproof but I don't particularly like it. Something with 'derivation' in it, perhaps.

Anyone any ideas?