A1, ..., An |- t
---------------------------- DISCH_ALL
|- A1 ==> ... ==> An ==> t
FAILURE
DISCH_ALL never fails. If there are no hypotheses to discharge, it will
simply return the theorem unchanged.
COMMENTS
Users should not rely on the hypotheses being discharged in any particular
order. Two or more alpha-convertible hypotheses will be discharged by a
single implication; users should not rely on which hypothesis appears in the
implication.