reactive "sledgehammer_filter": statically correct, but untested (no proof_file);