def add_successor

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:367

import Base

367def add_successor(+fuel: Nat, +cursor: Nat) -> {Nat.add(fuel, 1n+cursor) == 1n+Nat.add(fuel, cursor) : Nat}:
368  match fuel:
369    case 0n:
370      {==}
371    case 1n+tail:
372      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(tail, 1n+cursor), 1n+Nat.add(tail, cursor), add_successor(tail, cursor))