def swap

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32alg.bend:312

import Base

312# a + (b + c) == b + (a + c)
313def swap(+a: U32, +b: U32, +c: U32) -> {U32.add(a, U32.add(b, c)) == U32.add(b, U32.add(a, c)) : U32}:
314  %assoc(a, b, c) : {_ == U32.add(b, U32.add(a, c)) : U32}
315  %assoc(b, a, c) : {U32.add(U32.add(a, b), c) == _ : U32}
316  %U32.add_comm(a, b) : {U32.add(U32.add(a, b), c) == U32.add(_, c) : U32}
317  {==}