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?

P = coNP, which is equivalent to P = NP.

Right - those are equivalent.