theorem Cedar.Thm.var_entity_reachable {var : Spec.Var} {v : Spec.Value} {n : Nat} {request : Spec.Request} {entities : Spec.Entities} {euid : Spec.EntityUID} {path : List Spec.Attr} (he : Spec.evaluate (Spec.Expr.var var) request entities = Except.ok v) (ha : Value.EuidViaPath v path euid) (hf : Data.Map.contains entities euid = true) : ReachableIn entities request.sliceEUIDs euid (n + 1)