def pr3

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/point.bend:247

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg

247# the results are reduced
248def pr3(+one: Nat, +a: List<&2, Nat>, +b: List<&2, Nat>, +c: List<&2, Nat>, +ha: {red(one, a) == True{} : Bool}, +hb: {red(one, b) == True{} : Bool}, +hc: {red(one, c) == True{} : Bool}) -> {pred(one, P.Point{a, b, c}) == True{} : Bool}:
249  Lg.and_intro(red(one, a), Bool.and(red(one, b), red(one, c)), ha, Lg.and_intro(red(one, b), red(one, c), hb, hc))