def source_unchanged
stelliferous@0.0.2.0 · proofs/traversal_witness.bend:92
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
import Base
92def source_unchanged(~Reader: Type,~Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>,
93 evidence: ResultEvidence<Reader,Element,reader,depth,result>) -> {first(~Reader,~Array<Element>,result) == reader : Reader}:
94 match evidence:
95 case ResultEvidence{output,equation,output_evidence}:
96 Equal.cong(Reader & Array<Element>,Reader,pair => first(~Reader,~Array<Element>,pair),result,(reader,output),equation)