I don't understand you computation. I understand that you can replace the universal quantification on p' with only one of the cofactors, since the other one is trivial, but the same is not true for the second quantification on q'. If you don't like the example solution, then you probably want the following one:
∀p'. ∀q'. ( ((p↔q) ∨ (p'⊕q')) ∧ ((p↔q')∨(p'⊕q)) ) -> p'
= ∀q'. ( ((p↔q) ∨ (0⊕q')) ∧ ((p↔q')∨(0⊕q)) ) -> 0
= ∀q'. !( ((p↔q) ∨ q') ∧ ((p↔q')∨q) )
= !( ((p↔q) ∨ 0) ∧ ((p↔0)∨q) )
& !( ((p↔q) ∨ 1) ∧ ((p↔1)∨q) )
= !( (p↔q) ∧ (!p∨q) )
& !( 1 ∧ (p∨q) )
= !((p↔q) ∧ (!p∨q)) & !(p∨q)
= !((p↔q) ∧ (!p∨q)) & !p∧!q
= !((0↔0) ∧ (!0∨0)) & !p∧!q
= !(1 ∧ 1) & !p∧!q
= !1 & !p∧!q
= 0 & !p∧!q
This time, the result is as given in the example solution, namely false.
The change from universal to existential quantifiers is due to shifting the negation inside. Note that we have ¬ ∀x.phi = ∃x. ¬phi