Proof.rej_c: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/proof.bend as Proof
Lines 116-123 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/proof.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/proof.bend&start_line=116&end_line=123

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as SS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as SW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as M

def rej_c(+key: List<&2, U32>, +msg: List<&2, U32>, +tag: List<&2, U32>, h: {tag != R.mac(key, msg) : List<&2, U32>}, +c: Bool, +hc: {SS.equal(P.mac(key, msg), tag) == c : Bool}) -> {Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)) == False{} : Bool}:
  match c:
    case True{}:
      Empty.absurd({Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)) == False{} : Bool},
        h(Equal.trans(List<&2, U32>, tag, P.mac(key, msg), R.mac(key, msg), Equal.sym(List<&2, U32>, P.mac(key, msg), tag, equal_sound(P.mac(key, msg), tag, hc)), M.mac_correct(key, msg))))
    case False{}:
      Equal.trans(Bool, Bool.and(P.has_key(key), SS.equal(P.mac(key, msg), tag)), Bool.and(P.has_key(key), False{}), False{},
        Equal.cong(Bool, Bool, b => Bool.and(P.has_key(key), b), SS.equal(P.mac(key, msg), tag), False{}, hc), SW.and_false(P.has_key(key)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend&name=mac_correct
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/proof.bend&name=equal_sound
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend&name=and_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend&name=mac
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend&name=equal
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend&name=has_key
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend&name=mac