Simplifying a proof in our book

In [0], pp.66-69, we show how the conditional distribution of ∧ over ∀ can be derived from the one-point rule and the other axioms. I dragged sets into the picture, for which misbehaviour I apologize; here is a simpler argument. Representing “the non-empty range” for the dummy x by r.x ∨ [x=y] we show

[〈∀x : r.x ∨ [x=y]: t.x ∧ Q〉 ≡ 〈∀x : r.x ∨ [x=y]: t.x〉∧ Q ]

To this end we observe

〈∀x: r.x ∨ [x=y]: t.x ∧ Q〉

= {splitting the term}

〈∀x: r.x ∨ [x=y]: t.x〉 ∧ 〈∀x: r.x ∨ [x=y]: Q〉

= {see (*) below}

〈∀x: r.x ∨ [x=y]: t.x〉 ∧ Q

(*) We observe

〈∀x: r.x ∨ [x=y]: Q〉

= {splitting the range}

〈∀x: r.x: Q〉∧〈∀x: [x=y]: Q〉

= {one-point rule}

〈∀x: r.x: Q〉∧ Q

= {see (**) below)

Q

(**) We observe

[Q ⇒〈∀x:r.x: Q〉]

= { ⇒ distributes —like ∨— over ∀ in consequent}

[〈∀x: r.x: Q ⇒ Q〉]

= {pred. calc}

[〈∀x: r.x: true〉]

= {pred. calc., e.g. [0], p.66, (90)]

[true]

= {pred. calc.}

true

[0] Edsger W. Dijkstra & Carel S. Scholten Predicate Calculus and Program Semantics, Springer-Verlag New York Inc., 1990