Add theorem proving, impl strat, syntax, sc ideas

Describe notes and goals for theorem proving, implementation strategy, a
simple macro system via preprocessing, and vectorization ideas to
improve call-by-value supercompilation.