Tensor.nat_eq_succ: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/tensor.bend as Tensor
Lines 102-107 of bendtorch@1.3.0.0/tensor.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/tensor.bend&start_line=102&end_line=107

import Base

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

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat