Work on entailment toplevel.

Appears to be working but needs more tests.