def csh

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

28def csh(+k: Nat, +a: Nat, +b: Nat, +e: {a == b : Nat}) -> {C.shift(k, a) == C.shift(k, b) : Nat}:
29  Equal.cong(Nat, Nat, t => C.shift(k, t), a, b, e)