I assume you’re thinking of this—P=coNP ⇒ polytime decision for propositional tautologies (but not for mixed quanitifier bool. formulas). It’s CoNP-complete to decide tautologies (implicit forall for all the prop. vars) and NP-complete to decide satisfiability (implicit exists for all the prop. vars).
I don’t understand what you mean by “arbitrary verification procedures”—maybe you’re talking about a different result than the one I linked above?
I assume you’re thinking of this—P=coNP ⇒ polytime decision for propositional tautologies (but not for mixed quanitifier bool. formulas). It’s CoNP-complete to decide tautologies (implicit forall for all the prop. vars) and NP-complete to decide satisfiability (implicit exists for all the prop. vars).
I don’t understand what you mean by “arbitrary verification procedures”—maybe you’re talking about a different result than the one I linked above?
Right—those are equivalent.