def some_injective

bendtorch-core@0.1.0.0 · src/autograd/reduce_to_fold_PROOF.bend:118

import bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend as ReduceToFoldPROOF

import Base

118def some_injective(-A: Type, -x: A, -y: A, equal: {Some{x} == Some{y} : Maybe<&1, A>}) -> {x == y : A}:
119  Equal.cong(Maybe<&1, A>, A, found => Maybe.default(&1, A, found, x), Some{x}, Some{y}, equal)

Uses (3)

Maybe
Equal.cong
Maybe.default

Used by (0)

No other definition uses this definition.