Phc.append_nil: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc
Lines 1342-1347 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend&start_line=1342&end_line=1347

import Base

def append_nil(+x: String) -> {String.append(x, SNil{}) == x : String}:
  match x:
    case SNil{}:
      {==}
    case SCon{+h, +t}:
      Equal.cong(String, String, z => SCon{h, z}, String.append(t, SNil{}), t, append_nil(t))

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