def and_assoc

bend-collections-laws-math@1.0.0.0 · proofs/math/number/prime.bend:79

import Base

79# nodiv(1 + k, n, d) adds the test of d + k
80def and_assoc(+x: Bool, +y: Bool, +z: Bool) -> {Bool.and(x, Bool.and(y, z)) == Bool.and(Bool.and(x, y), z) : Bool}:
81  match x:
82    case True{}:
83      {==}
84    case False{}:
85      {==}