AESStringEqProof.cmp_eq_of_true: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend as AESStringEqProof
Lines 13-18 of qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend&start_line=13&end_line=18

import Base

def cmp_eq_of_true(c: Cmp,
    accepted: {Cmp.is_eq(c) == True{} : Bool}) -> {c == EQ{} : Cmp}:
    match c:
        case EQ{}: {==}
        case LT{}: Empty.absurd({LT{} == EQ{} : Cmp}, false_true(accepted))
        case GT{}: Empty.absurd({GT{} == EQ{} : Cmp}, false_true(accepted))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_StringEqProof.bend&name=false_true