Optlang: Fix up pure expressions and their eval relation
Optlang: Add op support to pure expressions
Optlang: Start proving nesting preservation

Still early days so far, but have reduced some cases to a proof that
it is preserved by eval, which is also started.