def btrue

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/arith.bend:31

import Base

31# Bool rewriting of a proposition {x == True}
32def btrue(+x: Bool, +y: Bool, +e: {x == y : Bool}, +h: {y == True{} : Bool}) -> {x == True{} : Bool}:
33  Equal.trans(Bool, x, y, True{}, e, h)