In demo:
- Also display the E interpolants for K and GL
- Let user choose what variable to quantify over
- Allow any letters as variable names
- Add support for inputting diamond.
Various optimizations:
- Avoid displaying double negations in the classical case
- Show neg bot as top.
- Use that (bot -> A) = top and (top -> A) = A and (A -> top) = top.
- More ambitious: Integrate an equivalence/normal form algorithm?