ProofShape.size_w.node: def of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 28-30 of lawful-arrays@0.1.0.0/proof_shape.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&start_line=28&end_line=30

import Base
import lawful-arrays@0.1.0.0/proof_tree.bend as P

def size_w.node(-T: Type, -xs: Array<T>, ys: Array<T>, w: SizeW(T, xs)) -> SizeW(T, ANode{xs, ys}):
  (b, n, e, q) = w
  (ANode{b, ys}, U32.shl(n), size_node_eq(T, xs, ys, b, n, e), P.anode_eq(T, b, ys, xs, ys, q, {==}))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shl
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=SizeW
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_shape.bend&name=size_node_eq
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=anode_eq