def dfs_or_some

minebender-game@1.0.0.0 · proof_solver.bend:1077

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S

1077def dfs_or_some(r: Maybe<&2, T.Grid(Bool)>, k: Unit -> Maybe<&2, T.Grid(Bool)>, -l: T.Grid(Bool),
1078  e: {S.dfs.or(r, k) == Some{l} : Maybe<&2, T.Grid(Bool)>}) ->
1079  Or({r == Some{l} : Maybe<&2, T.Grid(Bool)>}, {k(Unit{}) == Some{l} : Maybe<&2, T.Grid(Bool)>}):
1080  match r:
1081    case None{}:
1082      Inr{e}
1083    case Some{x}:
1084      Inl{e}