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

import Base

law hi_eq:
  for -T: Type
  for -xs: Array<T>
  for -r: Array<T> & T
  for -na: Array<T>
  for -old: T
  for e: {r == (na, old) : Array<T> & T}
  {Array.swap.hi(T, xs, r) == (ANode{xs, na}, old) : Array<T> & T}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.swap.hi
  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