nil by t, x
by nil for any other explicit value x, (not x) by x, and any other x
by (not x).
switch a hypothesis with the conclusion, negating both
Major Section: PROOF-CHECKER-COMMANDS
Example: (contrapose 3)The (optional) argumentGeneral Form: (contrapose &optional n)
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).