Proof by Defunctionalization

• small_step_interp
• diff_elements_tree
• tree_height