def string_eq_self

qasim-bend-kit@0.1.0.2 · proof/AES_StringEqProof.bend:35

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as Compare

35def string_eq_self(+s: String) ->
36    {String.eq(s, s) == True{} : Bool}:
37    Equal.cong((String & String) & Cmp, Bool,
38        result => Cmp.is_eq(Pair.snd(String & String, Cmp, result)),
39        String.cmp(s, s), ((s, s), EQ{}),
40        Compare.string_compare_self(s))