` `

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 `n`

th hypothesis, while negating the current `n`

th
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)`

.