Strengthen some of the lemmas in computation
Fixed some merge conflicts.
Caching done, with a simple example in ADTExamples.v
The example needs to be streamlined more, and the code in
ADTRefinement could use some cleaning up as well.
Updated TODO to reflect meeting Thursday, Feb. 6th.
Add some more computation lemmas
Redid caching per Adam's suggestions. Result is *much* simpler.
Add some more refinement helper instances
Add an observer-only refinement
Pulled out cache refinement into a separate file; updated makefile
accordingly.
Merge branch 'master' of file://///afs/csail.mit.edu/group/plv/git/adt-synthesis
Added a more general ADT refinement for refining mutator methods.
More general refinements in  ADTRefinement.
Redid Cache Example.
Still need to clean
Cleaned up the example derivation of the min collection; new tactics and
notation.
Make Sharpened an alias, not a symbol
- Improved refinement tactics to produce readable terms.