Start by removing files.
pausing on this, because it isn't going to work

- During reification the denotation function is determined
  after the full term is reified.
finished the migration.
working on LambdaM
eliminate type_weaken

- type_weaken is not implementable when types are not total, or
  we just need an appropriate default.
working on porting Ext

- The RType formulation is really painful now because nothing
  unifies anymore.
more porting.
Lambda compiles now.
Moving the implementations of symbols.

- Also splitting SymSum out of SymI.
A simple default prover that doesn't prove anything.
A more fuel efficient unification procedure.
An FMap for Uvars that is canonical by conversion
to positives.
updating the gitignore file to ignore #xxxx.xx#
a better proof (fewer universe constraints)

- It is a little bit scary that these universes break so quickly..
rename branch to stac.
local definition for resolution.
more tactics
Folding without types.
Several bug fixes!

- These were bad bugs
- There might be more, things still are not working
another bug in apply.

- Things might actually be working now.