S-design-memo-0
Proof is verification of sequence of ASTs
User defined items
The users need to define their own variables, functions, axioms, theorems
The users need to apply theorems in thier proofs
Modules
The users need to import variables, functions, axioms, theorems from other files, sometimes over the network
#s