def some_injective

bendtorch-core@0.1.0.0 · src/shape/plan_proofs.bend:28

import Base

28def some_injective(-A: Data, -x: A, -y: A, equal: {Some{x} == Some{y} : Maybe<&2, A>}) -> {x == y : A}:
29  Equal.cong(Maybe<&2, A>, A, found => Maybe.default(&2, A, found, x), Some{x}, Some{y}, equal)