Start to formalize some pieces of harper's book.
Don't index expressions by their free variables.