Theorem at-nodes

• Type: An axiom
• Validity: The proof is valid.
• Features: s, ls,
• Comment:
• Used by: nodes-alloc, nodes-alloc-append, nodes-alloc-subseteq, nodes-append, nodes-at-alloc, nodes-write-refsize, prefix-imp-nodes-subset,
• Used by units in proved state: ablock-store-refsize-cons,
• Proof exists?: No