def add_assoc

mylsm-lsm-store@0.3.2.0 · src/Wal.bend:243

import Base

243def add_assoc(n1: Nat, n2: Nat, n3: Nat) -> {Nat.add(Nat.add(n1, n2), n3) == Nat.add(n1, Nat.add(n2, n3)) : Nat}:
244  match n1:
245    case 0n:
246      {==}
247    case 1n+m:
248      %add_assoc(m, n2, n3) : {1n+Nat.add(Nat.add(m, n2), n3) == 1n+_ : Nat}
249      {==}