ProofSolver.loop_some.found: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 2236-2255 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=2236&end_line=2255

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/solver.bend as S
import minebender-game@1.0.0.0/proof_grid.bend as PG

def loop_some.found(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
  +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos,
  r: Or({c0 == c : T.Pos} & {S.search(c0, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>},
    Exists(T.Grid(Bool), l => {S.search(c0, todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} &
      {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>})),
  ih: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c)) ->
  LoopSome(c0 <> t, todo, part, ctx, c):
  match r:
    case Inl{pr}:
      match pr:
        case (cc, sn):
          %cc : {Bool.or(B.same(c0, _), B.contains(t, _)) == True{} : Bool} &
            {S.search(_, todo, part, ctx) == None{} : Maybe<&2, T.Grid(Bool)>}
          (or_l(B.same(c0, c0), B.contains(t, c0), PG.same_refl(c0)), sn)
    case Inr{ex}:
      match ex:
        case (l, pr):
          match pr:
            case (sl, lp):
              loop_some.lift(c0, t, todo, part, ctx, c, ih(l, lp))

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Either
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Exists
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=contains
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_grid.bend&name=same_refl
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=LoopSome
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=loop_some.lift
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=or_l
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Ctx
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=loop
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=search
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos