def reverse_go_append

qasim-bend-kit@0.1.0.2 · proof/JSON_StringProof.bend:17

import Base

17def reverse_go_append(+text: String,
18                      +acc: String,
19                      +suffix: String) -> {String.reverse.go(text, acc ++ suffix) == String.reverse.go(text, acc) ++ suffix : String}:
20    match text:
21        case SNil{}: {==}
22        case SCon{head, tail}:
23            Equal.trans(String,
24                String.reverse.go(tail, SCon{head, acc ++ suffix}),
25                String.reverse.go(tail, SCon{head, acc} ++ suffix),
26                String.reverse.go(tail, SCon{head, acc}) ++ suffix,
27                {==},
28                reverse_go_append(tail, SCon{head, acc}, suffix))