ProofSeq.take_set: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_seq.bend as ProofSeq
Lines 61-66 of lawful-bytes@0.1.1.0/proof_seq.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_seq.bend&start_line=61&end_line=66

import Base

law take_set:
  for +xs: List<&2, U32>
  for +m: Nat
  for +i: Nat
  for +v: U32
  {List.take(&2, U32, List.set(&2, U32, xs, i, v), m) == List.set(&2, U32, List.take(&2, U32, xs, m), i, v) : List<&2, U32>}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32