Equational theory for ThunkLang

[hrutvik]

PureLang's equational theory simplifies some of its compiler proofs considerably. We should introduce a theory for ThunkLang, to simplify verification of its future passes. ThunkLang is call-by-value, so (untyped) step-indexed logical relations would appear to be a good fit. We would need only soundness of contextual equivalence (not completeness like PureLang).