def some_equal

bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:90

import Base

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