To Do List
----------

- Add Sigma-types.
- Define natural numbers, lists, inductive datatypes from first principles. The goal is to use the HOL/Isabelle approach.
- Generic Tableaux prover.
- [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework.
- Independent type checker using a different programming language (e.g., F* or OCaml).
- Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.