proofs/lib/lemmas/proofs/public_config.bend checks

import Base
import ../src/cache.bend as C
import ../src/public.bend as Pub
import ../src/driver.bend as D
import ../spec/cache.bend as S
import ../spec/clock.bend as Clock
import ../spec/public_commands.bend as PC
import ../spec/equivalence.bend as E
import ../types/model.bend as T
import ./refinement.bend as F
import ./invariants.bend as Inv
import ./public_relation.bend as R
import ./public_drive.bend as Drive
import ./extensional_states.bend as Ext
import ./configuration_observations.bend as Config
import ./representation_access.bend as Access
import ./cache_storage_preservation.bend as Storage
import ./abstraction_size.bend as Size
import ./abstraction_bindings.bend as B