This file proves that typechecking of .extHasAttr expressions is sound.

theorem Cedar.Thm.type_of_extHasAttr_is_sound {x₁ : Spec.Expr} {a : Spec.Attr} {attrs : List Spec.Attr} {c₁ c₂ : Validation.Capabilities} {env : Validation.TypeEnv} {ty : Validation.TypedExpr} {request : Spec.Request} {entities : Spec.Entities} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : InstanceOfWellFormedEnvironment request entities env) (h₃ : Validation.typeOf (x₁.extHasAttr a attrs) c₁ env = Except.ok (ty, c₂)) (ih : TypeOfIsSound x₁) : GuardedCapabilitiesInvariant (x₁.extHasAttr a attrs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (x₁.extHasAttr a attrs) request entities v ∧ InstanceOfType env v ty.typeOf