Reduces a goal to implication from a known theorem.
DESCRIPTION
When applied to the theorem A' |- s and the goal A ?- t, the tactic
MP_TAC reduces the goal to A ?- s ==> t. Unless A' is a subset of
A, this is an invalid tactic.
A ?- t
============== MP_TAC (A' |- s)
A ?- s ==> t