Add interpreter with fuel

[j-f-ox]

Contents

• Fixes and proves previously incorrect multistep_preservation result
• Changes interpret to have a decreasing fuel parameter as discussed in class
• Proves main result

theorem interpreter_returns_exactly_normal_forms  :
  (well_typed: [] ⊢ t : T) ->
  ((t ~~>* t') ∧ (IsValue t')) ↔ (∃n, interpret n t = some t') := by