ACL2-PC::CONTRADICT

(macro) same as contrapose
Major Section:  PROOF-CHECKER-COMMANDS

see documentation for contrapose