ROADMAP

- Multi-file documents 
   - Imports
   - Persistence to local storage
   - Submission to server?
   - Lockable regions
- Elimination rules and induction
   - Defining inductive sets via grammar
- Equality and Definitions (Rayhana)
   - Definitions that are stricter than axioms.
   - Inductive definitions
   - Transitive calculational proofs IN PROGRESS
   - Rewriting in assumptions
   - Rewriting to use transitivity when rewriting on an equality proof.
- Built-ins
   - Strings
   - Naturals
- Hidden premises
   - e.g. a variable called "xs" in a rule implicity introduces a premise "xs List" but this is not usually displayed prominently and proofs attempt to solve it automatically.