LAWS.get_pair: law of lawful-arrays@0.1.0.0
Import: import lawful-arrays@0.1.0.0/LAWS.bend as LAWS
Lines 170-175 of lawful-arrays@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=lawful-arrays@0.1.0.0/LAWS.bend&start_line=170&end_line=175

import Base

# Array.get as a literal pair (so code that destructures it can be rewritten).
law get_pair:
  for -T: Data
  for a: Array<T>
  for i: U32
  {Array.get(T, a, i) == (a, Pair.snd(Array<T>, T, Array.get(T, a, i))) : Array<T> & T}

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.get
  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
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/PROOF.bend&name=get_pair.go
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_tree.bend&name=mirror