In , Mitchell Wand demonstrated that adding fexprs to the pure lambda calculus trivializes the theory of contextual equivalence, meaning two terms are contextually equivalent iff they are $\alpha$-congruent. When exploring related work, he went "our result extends an old observation of Albert Meyer  that
quote render contextual equivalence trivial". But referring to , what could be found is only the following statement by Meyer:
I ﬁrst thought that in languages with a
evalfeature such as LISP  there was no type distinction between syntactic and executable objects. In fact
evalseems safe enough in LISP because, although
quotesyntactically looks like a bona ﬁde operator, like say
cond, it really doesn’t behave like one (it only has behavior at parse time, not run time, e.g., one can't pass
quoteas a parameter to a procedure). Still, I have yet to see convincing examples where the
evalfeature was worthwhile.
Regardless of one minor flaw in these comments that may mislead the reader to infer that
cond could be passed as a parameter to a procedure. If I understand correctly, what Meyer said "
eval seems safe enough" means that
eval may not trivialize the equational theory, although he did not offer a proof.
As suggested by Martin, since all the three papers cited dealing with LISP family languages, let's put the question under this same setting. Is contextual equivalence of a language with
eval, in particular LISP, on earth trivial or not?
 Mitchell Wand, The Theory of Fexprs Is Trivial. Lisp and Symbolic Computation 10(3): 189-199 (1998).
 Albert Meyer, Puzzles in Programming Logic Workshop on Formal Software Development. 1984
 John McCarthy, Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I. Communications of the ACM in April 1960.