ACL2-PC::CONTRADICT
(macro)
same as
contrapose
Major Section:
PROOF-CHECKER-COMMANDS
see documentation for
contrapose