This file contains basic utility theorems used in the TPE soundness proof.

theorem Cedar.Thm.asValue_some {r : Spec.Residual} {v : Spec.Value} : r.asValue = some v ↔ ∃ (ty : Validation.CedarType), r = Spec.Residual.val v ty

theorem Cedar.Thm.isError_true {r : Spec.Residual} : r.isError = true ↔ ∃ (ty : Validation.CedarType), r = Spec.Residual.error ty

theorem Cedar.Thm.asValue_evaluate_val {r : Spec.Residual} {v : Spec.Value} : r.asValue = some v → ∀ (req : Spec.Request) (es : Spec.Entities), r.evaluate req es = Except.ok v

theorem Cedar.Thm.isError_evaluate_err {r : Spec.Residual} : r.isError = true → ∀ (req : Spec.Request) (es : Spec.Entities), ∃ (e : Spec.Error), r.evaluate req es = Except.error e