LAWS.list_take_append: law of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/LAWS.bend as LAWS
Lines 37-40 of bend-osdev-mode-core@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/LAWS.bend&start_line=37&end_line=40

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

law list_take_append:
  for +a: List<&2, U32>
  for +b: List<&2, U32>
  {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&name=li.take_append