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

import Base

law lo_eq:
  for -T: Type
  for -ys: Array<T>
  for -r: Array<T> & T
  for -na: Array<T>
  for -old: T
  for e: {r == (na, old) : Array<T> & T}
  {Array.swap.lo(T, ys, r) == (ANode{na, ys}, 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.lo
  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