def nat_eq_succ

bendtorch@1.3.0.0 · tensor.bend:102

import Base

102def nat_eq_succ(-a: Nat, -b: Nat, m: Maybe<&1, {a == b : Nat}>) -> Maybe<&1, {1n+a == 1n+b : Nat}>:
103  match m:
104    case Some{e}:
105      Some{Equal.cong(Nat, Nat, x => 1n+x, a, b, e)}
106    case None{}:
107      None{}