def append_assoc

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

import Base

11def append_assoc(+a: String, +b: String, +c: String) -> {(a ++ b) ++ c == a ++ (b ++ c) : String}:
12    match a:
13        case SNil{}: {==}
14        case SCon{h, t}:
15            Equal.cong(String, String, s => SCon{h, s}, (t ++ b) ++ c, t ++ (b ++ c), append_assoc(t, b, c))