ProofGen.gen_first.found: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 227-238 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=227&end_line=238

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

def gen_first.found(+z: G.Zone, +fx: Nat, +fy: Nat, +w: Nat, +g: T.Grid(Bool),
  s: {G.gen.out(z, T.Pos{fx, fy}) == True{} : Bool},
  r: Exists(G.GenState, st2 => {List.get(&2, List<&2, Bool>, g, fy)
    == Some{G.gen.row(z, fy, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>})) ->
  {L.mine(g, T.Pos{fx, fy}) == False{} : Bool}:
  match r:
    case (st2, eq):
      %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, g, fy),
        Some{G.gen.row(z, fy, List.range(w), st2)}, eq) :
        {Maybe.default(&2, Bool, List.get(&2, Bool,
          Maybe.default(&2, List<&2, Bool>, _, Nil{}), fx), False{}) == False{} : Bool}
      gen_first.col(z, fx, fy, w, st2, s, Nat.is_lt(fx, w), {==})

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=List.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.range
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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/LAWS.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=GenState
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Zone
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.out
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.row
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=gen_first.col
  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