def some_inj32

bend-osdev-algo@0.1.0.0 · PROOF.bend:832

import Base

832def some_inj32(-a: U32, -b: U32, e: {Some{a} == Some{b} : Maybe<&2, U32>}) -> {a == b : U32}:
833  Equal.cong(Maybe<&2, U32>, U32, m => maybe32.get(m), Some{a}, Some{b}, e)