~/jendhub

def successor_injective

bendtorch-core@0.1.0.0 · src/tensor/word_injective.bend:62

import bendtorch-core@0.1.0.0/src/tensor/word_injective.bend as WordInjective
import Base

62def successor_injective(-left: Nat, -right: Nat, equal: {1n+left == 1n+right : Nat}) -> {left == right : Nat}:
63  Equal.cong(Nat, Nat, n => predecessor(n), 1n+left, 1n+right, equal)

Uses (3)

Used by (1)