ACL2-PC::CONTRAPOSE

(primitive) switch a hypothesis with the conclusion, negating both
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(contrapose 3)

General Form: (contrapose &optional n)

The (optional) argument n should be a positive integer that does not exceed the number of hypotheses. Negate the current conclusion and make it the nth hypothesis, while negating the current nth hypothesis and making it the current conclusion. If no argument is supplied then the effect is the same as for (contrapose 1).

Note: By ``negate'' we mean an operation that replaces nil by t, x by nil for any other explicit value x, (not x) by x, and any other x by (not x).