proofs/lib/lemmas/proofs/abstraction_lookup.bend checks

import Base
import ./representation_access.bend as Access
import ./cache_populated.bend as Pop
import ./cache_delete_membership.bend as D
import ./map_routing.bend as R
import ../src/cache.bend as C
import ../src/codec.bend as Codec
import ../types/model.bend as T
import ./refinement.bend as F
import ./abstraction_bindings.bend as B
import ./abstraction_identity.bend as Identity
import ./abstraction_recency.bend as Recency
import ./enumeration_suffix.bend as Enum
import ./cache_key_identity.bend as Key
import ./invariants.bend as Inv
import ./representation_parts.bend as Parts