theorem Cedar.Thm.sliceEUIDs_record_field {r : Data.Map Spec.Attr Spec.Value} {a : Spec.Attr} {next : Spec.Value} (hfind : r.find? a = some next) (uid : Spec.EntityUID) : uid ∈ next.sliceEUIDs → uid ∈ (Spec.Value.record r).sliceEUIDs

If next is found in record r at key a, then sliceEUIDs of next ⊆ sliceEUIDs of record.

theorem Cedar.Thm.sliceEUIDs_entity_attr {ed : Spec.EntityData} {a : Spec.Attr} {next : Spec.Value} (hfind : ed.attrs.find? a = some next) (uid : Spec.EntityUID) : uid ∈ next.sliceEUIDs → uid ∈ ed.sliceEUIDs

If next is found in entity data attrs at key a, then sliceEUIDs of next ⊆ entity's sliceEUIDs.