TraversalCertificate.fold_operation: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as TraversalCertificate
Lines 97-105 of stelliferous@0.0.2.0/proofs/traversal_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_certificate.bend&start_line=97&end_line=105

import Base
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

def fold_operation(~Reader: Type,~Accumulator: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
  ~operation: Metadata -> Reader -> Accumulator -> Reader & Accumulator,
  ~preserves: @metadata: Metadata -> @-reader: Reader -> @-initial: Accumulator -> ReaderCertificate(reader) ->
    {TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)) == reader : Reader},
  metadata: Metadata,-reader: Reader,-initial: Accumulator,proof_certificate: ReaderCertificate(reader),certificate: ReaderCertificate(reader)) ->
  ReaderCertificate(TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial))):
  %Equal.sym(Reader,TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)),reader,
    preserves(metadata,reader,initial,proof_certificate)) : ReaderCertificate(_)
  certificate

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=first