Compile evaluate

theorem compile_evaluate {x : Expr} {env : Env} {εnv : SymEnv} {t : Term} :  env ∼ εnv →  env.WellFormedFor x →  εnv.WellFormedFor x →  compile x εnv = .ok t →  evaluate x env.request env.entities ∼ t:= by  intros h₁ h₂ h₃ h₄  match x with  | .lit _             => exact compile_evaluate_lit h₄  | .var _             => exact compile_evaluate_var h₁ h₄  | .ite x₁ x₂ x₃      =>    have ih₁ := @compile_evaluate x₁    have ih₂ := @compile_evaluate x₂    have ih₃ := @compile_evaluate x₃    exact compile_evaluate_ite h₁ h₂ h₃ h₄ ih₁ ih₂ ih₃  | .and x₁ x₂         =>    have ih₁ := @compile_evaluate x₁    have ih₂ := @compile_evaluate x₂    exact compile_evaluate_and h₁ h₂ h₃ h₄ ih₁ ih₂  | .or x₁ x₂          =>    have ih₁ := @compile_evaluate x₁    have ih₂ := @compile_evaluate x₂    exact compile_evaluate_or h₁ h₂ h₃ h₄ ih₁ ih₂  | .unaryApp _ x₁     =>    have ih₁ := @compile_evaluate x₁    exact compile_evaluate_unaryApp h₁ h₂ h₃ h₄ ih₁  | .binaryApp _ x₁ x₂ =>    have ih₁ := @compile_evaluate x₁    have ih₂ := @compile_evaluate x₂    exact compile_evaluate_binaryApp h₁ h₂ h₃ h₄ ih₁ ih₂  | .getAttr x₁ _     =>    have ih₁ := @compile_evaluate x₁    exact compile_evaluate_getAttr h₁ h₂ h₃ h₄ ih₁  | .hasAttr x₁ _     =>    have ih₁ := @compile_evaluate x₁    exact compile_evaluate_hasAttr h₁ h₂ h₃ h₄ ih₁  | .set xs           =>    have ih : ∀ xᵢ ∈ xs, CompileEvaluate xᵢ := by      intro xᵢ _      exact @compile_evaluate xᵢ    exact compile_evaluate_set h₁ h₂ h₃ h₄ ih  | .record axs      =>    have ih : ∀ aᵢ xᵢ, (aᵢ, xᵢ) ∈ axs → CompileEvaluate xᵢ := by      intro aᵢ xᵢ h      have _ : sizeOf xᵢ < 1 + sizeOf axs := List.sizeOf_snd_lt_sizeOf_list h      exact @compile_evaluate xᵢ    exact compile_evaluate_record h₁ h₂ h₃ h₄ ih  | .call _ xs       =>    have ih : ∀ xᵢ ∈ xs, CompileEvaluate xᵢ := by      intro xᵢ _      exact @compile_evaluate xᵢ    exact compile_evaluate_call h₁ h₂ h₃ h₄ ih