theorem
Cedar.Thm.checked_eval_entity_reachable_ite
{request : Spec.Request}
{nmax : Nat}
{v : Spec.Value}
{euid : Spec.EntityUID}
{e₁ e₂ e₃ : Spec.Expr}
{n : Nat}
{c c' : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{entities : Spec.Entities}
{path : List Spec.Attr}
(hc : CapabilitiesInvariant c request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf (e₁.ite e₂ e₃) c env = Except.ok (tx, c'))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax path)
(he : Spec.evaluate (e₁.ite e₂ e₃) request entities = Except.ok v)
(ha : Value.EuidViaPath v path euid)
(hf : Data.Map.contains entities euid = true)
(ih₂ : CheckedEvalEntityReachable e₂)
(ih₃ : CheckedEvalEntityReachable e₃)
:
ReachableIn entities request.sliceEUIDs euid (n + 1)