proofs/containers/doubly_linked_list/insf.bend checks

import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/array.bend as AR
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/doubly_linked_list.bend as S
import ../../lib/u32div.bend as UD
import ../../../src/containers/doubly_linked_list.bend as D
import ../../../src/containers/internal/dlist_storage.bend as R
import ../../../src/containers/types/internal_dlist.bend as I
import ../../../src/containers/types/doubly_linked_list.bend as E
import ./state.bend as ST
import ./rel.bend as RL
import ./vals.bend as VA
import ./lv.bend as LV
import ./link.bend as LN
import ./insg.bend as IG
import ./ok.bend as OK
import ./insp.bend as IP
import ../../lib/nat_list.bend as NL
import ../../lib/links.bend as LK
import ../../lib/words32.bend as W32
import ../../lib/u32_tree.bend as UT