ProofShape.size_node_eq: law of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_shape.bend as ProofShape
Lines 14-21 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=14&end_line=21

import Base

law size_node_eq:
  for -T: Type
  for -xs: Array<T>
  for -ys: Array<T>
  for -b: Array<T>
  for -n: U32
  for e: {Array.size(T, xs) == (b, n) : Array<T> & U32}
  {Array.size(T, ANode{xs, ys}) == (ANode{b, ys}, U32.shl(n)) : Array<T> & U32}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.size
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.size.node
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shl