LAWS.octets_concat_cons: law of bend-osdev-bytes@0.1.1.0
Import: import bend-osdev-bytes@0.1.1.0/LAWS.bend as LAWS
Lines 229-232 of bend-osdev-bytes@0.1.1.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.0/LAWS.bend&start_line=229&end_line=232

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

law octets_concat_cons:
  for h: B.Octets
  for t: List<&2, B.Octets>
  {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/PROOF.bend&name=p_octets_concat_cons
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.append
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.concat