def know_row_get.some

minebender-game@1.0.0.0 · proof_grid.bend:28

import Base

28def know_row_get.some(-A: Data, +a: A, +x: A, e: {Some{a} == Some{x} : Maybe<&2, A>}) ->
29  {a == x : A}:
30  Equal.cong(Maybe<&2, A>, A, m => Maybe.value(A, a, m), Some{a}, Some{x}, e)