Draft: Proto/SORU: refactor refutation proofs' valid function to merge two pattern matchings

The reason of this refactoring is that for Adjustable DAL, we need Dal_helpers.verify to return some extra information in addition to input_opt (see !16132 (diffs)). With the previous implementation, we should modify all the other cases of the first pattern matching to return something (even if it's None), and then process it in the second pattern matching.

With this refactoring, where we only have one pattern matching and which performs all the checks, we'll only need to modify the DAL-related helper's return type.

For the review, it might be better to read the new implementation and, in parallel, 
the two old pattern matching and try to make/see a kind of bijection between the 
two implementations.