def append_nil

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

import Base

5def append_nil(+text: String) -> {text ++ SNil{} == text : String}:
6    match text:
7        case SNil{}: {==}
8        case SCon{h, t}:
9            Equal.cong(String, String, s => SCon{h, s}, t ++ SNil{}, t, append_nil(t))