Proves goal by asserting it as an axiom.
Given any goal A ?- p, the tactic CHEAT_TAC solves it by using mk_thm,
which in turn involves essentially asserting the goal as a new axiom.
- FAILURE CONDITIONS
Temporarily plugging boring parts of a proof to deal with the interesting
Needless to say, this should be used with caution since once new axioms are
asserted there is no guarantee that logical consistency is preserved.
- SEE ALSO