def some_inj

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/below.bend:86

import Base

86def some_inj(+x: Nat, +y: Nat, e: {Some{x} == Some{y} : Maybe<&2, Nat>}) -> {x == y : Nat}:
87  Equal.cong(Maybe<&2, Nat>, Nat, m => some_or(m, x), Some{x}, Some{y}, e)