def aes_string_append_assoc

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:461

import Base

461def aes_string_append_assoc(+a: String, +b: String, +c: String) ->
462    {a ++ b ++ c == a ++ (b ++ c) : String}:
463    match a:
464        case SNil{}: {==}
465        case SCon{head, tail}:
466            Equal.cong(String, String, rest => SCon{head, rest},
467                tail ++ b ++ c, tail ++ (b ++ c),
468                aes_string_append_assoc(tail, b, c))