def f_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/fprot.bend:59

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as F

59def f_eq(+a: List<&2, Nat>, +b: List<&2, Nat>) -> {F.eq(a, b) == L.eq(a, b) : Bool}:
60  Equal.trans(Bool, F.eq(a, b), F.eq_b(a, b), L.eq(a, b), f_eq_a(a, b), f_eq_b(a, b))