David,
There is a reason why the ProofPower tutorials don't say much about the
forward proof tools you are trying to use.
I have given courses on ProofPower HOL and on ProofPower Z and wrote the
tutorials.
What I did in the courses was to teach just enough about forward proof
for the students
Since the slides for this book use slightly different notation, I am back
to trying to implement the proofs in the main book: UsingZ from
www.usingz.com (in text link, it is zedbook)
On page 42, the proof is using nested existentials, and I am trying
to get past my lack of understanding in apply
