Doubt 1: (p' xor q') is equivalent to !(p'<->q'), so when we multiply out, we get

(((p<->q) | (p' xor q')) & ((p<->q')|(p' xor q))&(p'<->q'))
<->
(
(p<->q) & ((p<->q')|(p' xor q))&(p'<->q')
|(p' xor q') & ((p<->q')|(p' xor q)) & (p'<->q')
)
<->
(p<->q) & ((p<->q')|(p' xor q))&(p'<->q')

Note that (p' xor q') & (...) & (p'<->q') is just false.

Doubt 2:

exists q'. (p<->q) & ((p<->q')|(p' xor q)) & (p'<->q')
<-> (p<->q) & ((p<->0)|(p' xor q)) & (p'<->0)
| (p<->q) & ((p<->1)|(p' xor q)) & (p'<->1)
<-> (p<->q) & (!p|(p' xor q)) & !p'
| (p<->q) & ( p|(p' xor q)) & p'
<-> (p<->q) & (!p|(0 xor q)) & !p'
| (p<->q) & ( p|(1 xor q)) & p'
<-> (p<->q) & (!p| q) & !p'
| (p<->q) & ( p|!q) & p'

p' was omitted because of φ ∧ x ⇔ φ[x<-1] ∧ x and φ ∧ ¬x ⇔ φ[x<-0] ∧ x (see page 69 on the Chapter on transition systems where the symbolic computation of predecessors and successors is explained with this trick.