ACL2-pc::contrapose
(primitive)
switch a hypothesis with the conclusion, negating both
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).
Remark: 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).
