def succ_out

bend-ml-tensor-array@0.1.19.0 · main.bend:1789

import Base

1789# s == a + (1 + b)  ->  s == 1 + (a + b)
1790def succ_out(-s: Nat, +a: Nat, +b: Nat, e: {s == Nat.add(a, 1n+b) : Nat}) -> {s == 1n+Nat.add(a, b) : Nat}:
1791  %Equal.sym(Nat, 1n+Nat.add(a, b), Nat.add(a, 1n+b), add_succ_r(a, b)) : {s == _ : Nat}
1792  e