Residual well typed is sound

theorem residual_well_typed_is_sound {r : Residual} {v : Value} {env : TypeEnv} {request : Request} {entities : Entities} :  InstanceOfWellFormedEnvironment request entities env →  Residual.WellTyped env r →  r.evaluate request entities = .ok v →  InstanceOfType env v r.typeOf:= by  intro h₁ h₂ h₃  induction h₂ generalizing v <;> simp only [Residual.typeOf]  case val v ty h₄ =>    exact residual_well_typed_is_sound_val h₄ h₃  case var var ty h₄ =>    exact residual_well_typed_is_sound_var h₁ h₄ h₃  case ite x₁ x₂ x₃ h₁ h₂ h₃ h₄ h₅ h₆ hᵢ₁ hᵢ₂ =>    exact residual_well_typed_is_sound_ite h₄ h₅ h₆ hᵢ₁ hᵢ₂ h₃  case and x₁ x₂ _ _ h₄ h₅ hᵢ₁ hᵢ₂ =>    exact residual_well_typed_is_sound_and h₄ h₅ hᵢ₁ hᵢ₂ h₃  case or x₁ x₂ _ _ h₄ h₅ hᵢ₁ hᵢ₂ =>    exact residual_well_typed_is_sound_or h₄ h₅ hᵢ₁ hᵢ₂ h₃  case unaryApp op₁ x₁ ty _ h₄ hᵢ₁ =>    exact residual_well_typed_is_sound_unary_app h₄ hᵢ₁ h₃  case binaryApp op₂ x₁ x₂ ty _ _ h₄ hᵢ₁ hᵢ₂ =>    exact residual_well_typed_is_sound_binary_app h₁ h₄ hᵢ₁ hᵢ₂ h₃  case hasAttr_entity ety x₁ attr h₁ h₂ h₃ =>    exact residual_well_typed_is_sound_has_attr_entity h₃  case hasAttr_record rty x₁ attr h₁ h₂ h₃ =>    exact residual_well_typed_is_sound_has_attr_record h₃  case getAttr_entity ety rty x₁ attr ty h₄ h₅ h₆ h₇ hᵢ =>    exact residual_well_typed_is_sound_get_attr_entity h₁ hᵢ h₅ h₆ h₇ h₃  case getAttr_record rty x₁ attr ty h₄ h₅ h₆ hᵢ =>    exact residual_well_typed_is_sound_get_attr_record hᵢ h₅ h₆ h₃  case set ls ty h₄ h₅ h₆ h₇ =>    exact residual_well_typed_is_sound_set h₇ h₅ h₃  case record rty m hᵢ₁ h₄ hᵢ =>    exact residual_well_typed_is_sound_record hᵢ h₄ h₃  case call xfn args ty _ h₄ _ =>    exact residual_well_typed_is_sound_call h₄ h₃  case error ty =>    -- Error case should not produce a successful result    simp only [Residual.evaluate] at h₃    -- h₃ : Except.error Error.extensionError = Except.ok v    -- This is a contradiction since error ≠ ok    cases h₃