added the CBN version of evaluation as well and its progress proof. Also super easy induction.
Added some denotational semantics and trying to prove that the operational semantics respects the denotation function. I'm not entirely sure this will work in general without funext, but I'm also not completely sure of how this'll work. Need to finish the proof that it respects substitution which I think is going to be the hard part.