Using...Prove declarations

A using...prove declaration tells the verification system to use one assertion as an assumption when verifying another. A declaration of the form

        using foo prove bar;

where foo and bar are identifiers for assertions, tells the verification system to use assertion foo as an assumption when proving assertion bar. A list of assumptions may also be used:

        using a1,a2,...,an prove bar;

Such a ``proof'' may not contain circular chains of reasoning. Thus, for example,

        using foo prove bar;
        using bar prove foo;

is illegal.