proofs/lib/lemmas/proofs/oldest_refinement.bend checks

import Base
import ../src/cache.bend as C
import ../src/codec.bend as Codec
import ../spec/cache.bend as S
import ../spec/operations.bend as O
import ../spec/equivalence.bend as E
import ../types/model.bend as T
import ./refinement.bend as F
import ./invariants.bend as Inv
import ./disabled.bend as Disabled
import ./spec_lookup.bend as Lookup
import ./read_refinement.bend as Read
import ./remove_refinement.bend as Remove
import ./extensional_states.bend as Ext
import ./string_order.bend as Order
import ./abstraction_recency.bend as Recency