Type of is sound

theorem type_of_is_sound {e : Expr} {c₁ c₂ : Capabilities} {env : TypeEnv} {ty : TypedExpr} {request : Request} {entities : Entities} :  CapabilitiesInvariant c₁ request entities →  InstanceOfWellFormedEnvironment request entities env →  typeOf e c₁ env = .ok (ty, c₂) →  GuardedCapabilitiesInvariant e c₂ request entities ∧  ∃ (v : Value), EvaluatesTo e request entities v ∧ InstanceOfType env v ty.typeOf:= by  intro h₁ h₂ h₃  match e with  | .lit l => exact type_of_lit_is_sound h₃  | .var var => exact type_of_var_is_sound h₂ h₃  | .ite x₁ x₂ x₃ =>    have ih₁ := @type_of_is_sound x₁    have ih₂ := @type_of_is_sound x₂    have ih₃ := @type_of_is_sound x₃    exact type_of_ite_is_sound h₁ h₂ h₃ ih₁ ih₂ ih₃  | .and x₁ x₂ =>    have ih₁ := @type_of_is_sound x₁    have ih₂ := @type_of_is_sound x₂    exact type_of_and_is_sound h₁ h₂ h₃ ih₁ ih₂  | .or x₁ x₂ =>    have ih₁ := @type_of_is_sound x₁    have ih₂ := @type_of_is_sound x₂    exact type_of_or_is_sound h₁ h₂ h₃ ih₁ ih₂  | .unaryApp op₁ x₁ =>    have ih := @type_of_is_sound x₁    exact type_of_unaryApp_is_sound h₁ h₂ h₃ ih  | .binaryApp op₂ x₁ x₂ =>    have ih₁ := @type_of_is_sound x₁    have ih₂ := @type_of_is_sound x₂    exact type_of_binaryApp_is_sound h₁ h₂ h₃ ih₁ ih₂  | .hasAttr x₁ a =>    have ih := @type_of_is_sound x₁    exact type_of_hasAttr_is_sound h₁ h₂ h₃ ih  | .getAttr x₁ a =>    have ih := @type_of_is_sound x₁    exact type_of_getAttr_is_sound h₁ h₂ h₃ ih  | .set xs =>    have ih : ∀ xᵢ, xᵢ ∈ xs → TypeOfIsSound xᵢ := by      intro xᵢ _      exact @type_of_is_sound xᵢ    exact type_of_set_is_sound h₁ h₂ h₃ ih  | .record axs =>    have ih : ∀ axᵢ, axᵢ ∈ axs → TypeOfIsSound axᵢ.snd := by      intro axᵢ hᵢ      have _ : sizeOf axᵢ.snd < 1 + sizeOf axs := by        apply List.sizeOf_snd_lt_sizeOf_list hᵢ      exact @type_of_is_sound axᵢ.snd    exact type_of_record_is_sound h₁ h₂ h₃ ih  | .call xfn xs =>    have ih : ∀ xᵢ, xᵢ ∈ xs → TypeOfIsSound xᵢ := by      intro xᵢ _      exact @type_of_is_sound xᵢ    exact type_of_call_is_sound h₁ h₂ h₃ ih