~/jendhub

def append_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/phc.bend:1342

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc
import Base

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

Uses (3)

Used by (1)