PROOF.append_pair.go: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/PROOF.bend as PROOF
Lines 263-271 of lawful-bytes@0.1.1.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/PROOF.bend&start_line=263&end_line=271

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-bytes@0.1.1.0/proof_append.bend as X

def append_pair.go(-dst: D.Bytes, -src: D.Bytes, +s: U32, +n: U32, m_dst: C.BMirror(dst), m_src: C.BMirror(src)) ->
  {B.append(dst, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(dst, src, s, n)), src) : D.Bytes & D.Bytes}:
  (+l_dst, m2_dst) = m_dst
  (+t_dst, +e_dst) = m2_dst
  (+l_src, m2_src) = m_src
  (+t_src, +e_src) = m2_src
  %e_dst : {B.append(_, src, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(_, src, s, n)), src) : D.Bytes & D.Bytes}
  %e_src : {B.append(C.BT(l_dst, t_dst), _, s, n) == (Pair.fst(D.Bytes, D.Bytes, B.append(C.BT(l_dst, t_dst), _, s, n)), _) : D.Bytes & D.Bytes}
  X.append_pair_t(l_dst, t_dst, l_src, t_src, s, n)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  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-bytes@0.1.1.0/bytes.bend&name=append
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/defs.bend&name=Bytes
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_append.bend&name=append_pair_t
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=BMirror
  https://jend.leeeet.dev/definition.txt?path=lawful-bytes@0.1.1.0/proof_core.bend&name=BT