PROOF.p_octets_concat_cons: def of bend-osdev-bytes@0.1.1.0
Import: import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF
Lines 750-752 of bend-osdev-bytes@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bytes@0.1.1.0/PROOF.bend&start_line=750&end_line=752

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

def p_octets_concat_cons(+h: B.Octets, +t: List<&2, B.Octets>) -> {B.Octets.concat(Con{h, t}) == B.Octets.append(h, B.Octets.concat(t)) : B.Octets}:
  %Equal.sym(B.Octets, B.Octets.concat(t), B.Octets.concat.ref(t), concat_ref(t)) : {B.Octets.concat(Con{h, t}) == B.Octets.append(h, _) : B.Octets}
  concat_ref(Con{h, t})

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=concat_ref
  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
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.0/bytes.bend&name=Octets.concat.ref