ProofTree.size_eta: law of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTree
Lines 110-113 of lawful-arrays@0.1.0.0/proof_tree.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&start_line=110&end_line=113

import Base

law size_eta:
  for -T: Type
  for a: Array<T>
  {Array.size(T, a) == (a, Pair.snd(Array<T>, U32, Array.size(T, a))) : 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=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32