AESEnvelopeProof.aes_string_append_assoc: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 461-468 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=461&end_line=468

import Base

def aes_string_append_assoc(+a: String, +b: String, +c: String) ->
    {a ++ b ++ c == a ++ (b ++ c) : String}:
    match a:
        case SNil{}: {==}
        case SCon{head, tail}:
            Equal.cong(String, String, rest => SCon{head, rest},
                tail ++ b ++ c, tail ++ (b ++ c),
                aes_string_append_assoc(tail, b, c))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append