Conversion preserves evaluation

theorem conversion_preserves_evaluation (te : TypedExpr) (req : Request) (es : Entities) :  Spec.evaluate te.toExpr req es = (TypedExpr.toResidual te).evaluate req es := by  cases te with  | lit p ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]  | var v ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual]    cases v <;> simp [Spec.evaluate, Residual.evaluate]  | ite cond thenExpr elseExpr ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih_cond := conversion_preserves_evaluation cond req es    have ih_then := conversion_preserves_evaluation thenExpr req es    have ih_else := conversion_preserves_evaluation elseExpr req es    rw [←ih_cond]    simp [Result.as, Value.asBool]    rw [←ih_then, ←ih_else]    cases Spec.evaluate cond.toExpr req es    case ite.error =>      simp    case ite.ok =>      simp      rename_i a      cases a      case prim =>        simp [bind, Coe.coe, Value.asBool]      all_goals {        simp [Coe.coe, Value.asBool]      }  | and a b ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih_a := conversion_preserves_evaluation a req es    have ih_b := conversion_preserves_evaluation b req es    rw [←ih_a, ←ih_b]  | or a b ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih_a := conversion_preserves_evaluation a req es    have ih_b := conversion_preserves_evaluation b req es    rw [←ih_a, ←ih_b]  | unaryApp op expr ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih := conversion_preserves_evaluation expr req es    rw [←ih]  | binaryApp op a b ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih_a := conversion_preserves_evaluation a req es    have ih_b := conversion_preserves_evaluation b req es    rw [←ih_a, ←ih_b]  | getAttr expr attr ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih := conversion_preserves_evaluation expr req es    rw [←ih]  | hasAttr expr attr ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    have ih := conversion_preserves_evaluation expr req es    rw [←ih]  | set ls ty =>    unfold TypedExpr.toExpr    simp [TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    congr 1    rw [List.map₁_eq_map, List.map₁_eq_map]    rw [List.mapM₁_eq_mapM (Spec.evaluate · req es)]    rw [List.mapM₁_eq_mapM (Residual.evaluate · req es)]    rw [List.mapM_map, List.mapM_map]    rw [List.forall₂_implies_mapM_eq]    apply conversion_preserves_evaluation_forall2  | record map ty =>    unfold TypedExpr.toExpr    simp [TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    congr 1    rw [List.mapM₂_eq_mapM λ x => bindAttr x.fst (Spec.evaluate x.snd req es)]    rw [List.map₂_eq_map_snd TypedExpr.toExpr]    rw [List.map₂_eq_map_snd TypedExpr.toResidual]    rw [List.mapM₂_eq_mapM λ x => bindAttr x.fst (Residual.evaluate x.snd req es)]    unfold bindAttr    rw [List.mapM_map, List.mapM_map]    simp    rw [List.forall₂_implies_mapM_eq]    apply conversion_preserves_evaluation_forall2_map  | call xfn args ty =>    simp [TypedExpr.toExpr, TypedExpr.toResidual, Spec.evaluate, Residual.evaluate]    congr 1    rw [List.map₁_eq_map, List.map₁_eq_map]    rw [List.mapM₁_eq_mapM (Spec.evaluate · req es), List.mapM₁_eq_mapM (Residual.evaluate · req es)]    rw [List.mapM_map, List.mapM_map]    rw [List.forall₂_implies_mapM_eq]    apply conversion_preserves_evaluation_forall2