law reify_node

bend-collections@1.0.0.0 · proofs/crypto/sha/packed/packed_array_proof.bend:18

import Base

18law reify_node:
19  for -l: Array<U32>
20  for -r: Array<U32>
21  for left: Sigma<&2,&1,Tree,t => {l == thaw(t) : Array<U32>}>
22  for right: Sigma<&2,&1,Tree,t => {r == thaw(t) : Array<U32>}>
23  Sigma<&2,&1,Tree,t => {ANode{l,r} == thaw(t) : Array<U32>}>