Added 'quoteGoal x by p in e' syntax
meaning, let x = p [current goal] in e
Additionally, the value of x is normalised, which means p can be a
compile-time only %reflection function used to prove something interesting
in e. See test030 for an example of automated proof by reflection.