use a clause-processor
Major Section: PROOF-CHECKER-COMMANDS
Example: (cl-proc :function note-fact-clause-processor :hint '(equal a a)) -- Invoke the indicated clause processor function with the indicated hint argument (see the beginning of fileInvoke a clause-processor as indicated by cl-proc-args, which is a list of arguments that can serve as the value of a
General Form: (cl-proc &rest cl-proc-args)
clause-processorhint; see hints.
This command calls the
prove command, and hence should only be used
at the top of the conclusion.