How does Typol assign initial values to a proposition? And how do we recover the result(s) of the proof? In almost all circumstances, abstract syntax trees that are initial values of propositions reside in Le-Lisp and must be sent to prolog, being coerced into a prolog term along the way. Results send by prolog are similarly coerced into Le-Lisp representations.