def some_inj

minebender-game@1.0.0.0 · proof_lists.bend:26

import Base

26def some_inj(-A: Data, +a: A, +x: A, e: {Some{a} == Some{x} : Maybe<&2, A>}) -> {a == x : A}:
27  Equal.cong(Maybe<&2, A>, A, m => Maybe.val(A, a, m), Some{a}, Some{x}, e)