Compile interpret

theorem compile_interpret {x : Expr} {εnv : SymEnv} {I : Interpretation} {t : Term} :  I.WellFormed εnv.entities →  εnv.WellFormedFor x →  compile x εnv = .ok t →  compile x (εnv.interpret I) = .ok (t.interpret I):= by  intros h₁ h₂ h₃  match x with  | .lit _             => exact compile_interpret_lit h₃  | .var _             => exact compile_interpret_var h₁ h₂ h₃  | .ite x₁ x₂ x₃      =>    have ih₁ := @compile_interpret x₁    have ih₂ := @compile_interpret x₂    have ih₃ := @compile_interpret x₃    exact compile_interpret_ite h₁ h₂ h₃ ih₁ ih₂ ih₃  | .and x₁ x₂         =>    have ih₁ := @compile_interpret x₁    have ih₂ := @compile_interpret x₂    exact compile_interpret_and h₁ h₂ h₃ ih₁ ih₂  | .or x₁ x₂          =>    have ih₁ := @compile_interpret x₁    have ih₂ := @compile_interpret x₂    exact compile_interpret_or h₁ h₂ h₃ ih₁ ih₂  | .unaryApp _ x₁     =>    have ih₁ := @compile_interpret x₁    exact compile_interpret_unaryApp h₁ h₂ h₃ ih₁  | .binaryApp _ x₁ x₂ =>    have ih₁ := @compile_interpret x₁    have ih₂ := @compile_interpret x₂    exact compile_interpret_binaryApp h₁ h₂ h₃ ih₁ ih₂  | .getAttr x₁ _      =>    have ih₁ := @compile_interpret x₁    exact compile_interpret_getAttr h₁ h₂ h₃ ih₁  | .hasAttr x₁ _      =>    have ih₁ := @compile_interpret x₁    exact compile_interpret_hasAttr h₁ h₂ h₃ ih₁  | .set xs            =>    have ih : ∀ xᵢ ∈ xs, CompileInterpret xᵢ := by      intro xᵢ _      exact @compile_interpret xᵢ    exact compile_interpret_set h₁ h₂ h₃ ih  | .record axs      =>    have ih : ∀ aᵢ xᵢ, (aᵢ, xᵢ) ∈ axs → CompileInterpret xᵢ := by      intro aᵢ xᵢ h      have _ : sizeOf xᵢ < 1 + sizeOf axs := List.sizeOf_snd_lt_sizeOf_list h      exact @compile_interpret xᵢ    exact compile_interpret_record h₁ h₂ h₃ ih  | .call _ xs       =>    have ih : ∀ xᵢ ∈ xs, CompileInterpret xᵢ := by      intro xᵢ _      exact @compile_interpret xᵢ    exact compile_interpret_call h₁ h₂ h₃ ih