theorem Cedar.Thm.is_eq_type_comparison_of_entity_type {env : Validation.TypeEnv} {v : Spec.Value} {ety₁ ety₂ : Spec.EntityType} (hinst : InstanceOfType env v (Validation.CedarType.entity ety₂)) : Spec.apply₁ (Spec.UnaryOp.is ety₁) v = Except.ok (Spec.Value.prim (Spec.Prim.bool (ety₁ == ety₂)))

is on an entity-typed value is decided by comparing the two types.

theorem Cedar.Thm.try_decide_residual₁_sound {env : Validation.TypeEnv} {r₁ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {op₁ : Spec.UnaryOp} {v : Spec.Value} (hwf : InstanceOfWellFormedEnvironment req es env) (hwt : Residual.WellTyped env r₁) (hdec : TPE.tryDecideResidual₁ op₁ r₁ = some v) : ∃ (v' : Spec.Value), r₁.evaluate req es = Except.ok v' ∧ Spec.apply₁ op₁ v' = Except.ok v

theorem Cedar.Thm.partial_evaluate_is_sound_unary_app {x₁ : Spec.Residual} {req : Spec.Request} {es : Spec.Entities} {preq : TPE.PartialRequest} {pes : TPE.PartialEntities} {op₁ : Spec.UnaryOp} {ty : Validation.CedarType} {env : Validation.TypeEnv} (h₂ : InstanceOfWellFormedEnvironment req es env) (hwt : Residual.WellTyped env x₁) (h_ref : RequestAndEntitiesRefine req es preq pes) (hᵢ₁ : Except.toOption (x₁.evaluate req es) = Except.toOption ((TPE.evaluate env x₁ preq pes).evaluate req es)) : Except.toOption ((Spec.Residual.unaryApp op₁ x₁ ty).evaluate req es) = Except.toOption ((TPE.evaluate env (Spec.Residual.unaryApp op₁ x₁ ty) preq pes).evaluate req es)