PROVE_HYP
Drule.PROVE_HYP : thm -> thm -> thm
Eliminates a provable assumption from a theorem.
When applied to two theorems, PROVE_HYP returns a theorem having the
conclusion of the second. The new hypotheses are the union of the two
hypothesis sets (first deleting, however, the conclusion of the first
theorem from the hypotheses of the second).
A1 |- t1 A2 |- t2
------------------------ PROVE_HYP
A1 u (A2 - {t1}) |- t2
Failure
Never fails.
Comments
This is the Cut rule. It is not necessary for the conclusion of the
first theorem to be the same as an assumption of the second, but
PROVE_HYP is otherwise of doubtful value.