ProofSpeed.when_or_eq: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_speed.bend as ProofSpeed
Lines 440-454 of minebender-game@1.0.0.0/proof_speed.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_speed.bend&start_line=440&end_line=454

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

def when_or_eq(+g0a: Bool, +g0b: Bool, eg0: {g0a == g0b : Bool},
  +d0a: Maybe<&2, T.Grid(Bool)>, +d0b: Maybe<&2, T.Grid(Bool)>, ed0: {d0a == d0b : Maybe<&2, T.Grid(Bool)>},
  +g1a: Bool, +g1b: Bool, eg1: {g1a == g1b : Bool},
  +d1a: Maybe<&2, T.Grid(Bool)>, +d1b: Maybe<&2, T.Grid(Bool)>, ed1: {d1a == d1b : Maybe<&2, T.Grid(Bool)>}) ->
  {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
    == S.dfs.or(S.dfs.when(g0b, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}:
  %eg0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
    == S.dfs.or(S.dfs.when(_, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
  %ed0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
    == S.dfs.or(S.dfs.when(g0a, x => _), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
  %eg1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(_, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
  %ed1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => _)) : Maybe<&2, T.Grid(Bool)>}
  {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.or
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.when
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid