ProofAssist.stuck_pick.none: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_assist.bend as ProofAssist
Lines 202-226 of minebender-game@1.0.0.0/proof_assist.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_assist.bend&start_line=202&end_line=226

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/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_base.bend as P
import minebender-game@1.0.0.0/proof_grid.bend as PG
import minebender-game@1.0.0.0/proof_copy.bend as PC
import minebender-game@1.0.0.0/proof_cells.bend as PS

def stuck_pick.none(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +s: T.Grid(Bool), +f: List<&2, T.Pos>, +k: Nat,
  sa: SafeAt(layout, s, G.safe_list(w, h, s, k))) ->
  Exists(T.Pos, p => {L.mine(layout, p) == False{} : Bool} &
    ({L.hidden(G.knowledge(G.Game{w, h, layout, s, f, T.Playing{}}), p) == True{} : Bool} &
     {G.assist.safe(G.first_safe(layout, s, G.safe_list(w, h, s, k)), G.Game{w, h, layout, s, f, T.Playing{}})
       == G.open(G.Game{w, h, layout, s, f, T.Playing{}}, p) : G.Game})):
  match sa:
    case (+p, pr):
      match pr:
        case (+fe, rest):
          match rest:
            case (+sf, m):
              +g0 = {G.Game{w, h, layout, s, f, T.Playing{}} : G.Game}
              +nm = P.not_true(B.mine(layout, p), P.and_true_l(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf))
              +onp = PS.allp_member(~PS.WH, ~PS.onb, PS.WH{w, h}, G.safe_list(w, h, s, k), p, on_list(w, h, s, k), m)
              (p,
                (%PC.mine_eq(layout, p) : {_ == False{} : Bool}; nm,
                 (%Equal.sym(Bool, L.hidden(G.knowledge(g0), p), G.unrevealed(w, h, s, p),
                    PG.know_hidden(w, h, layout, s, f, T.Playing{}, p)) : {_ == True{} : Bool};
                    %Equal.sym(Bool, B.on_board(w, h, p), True{}, onp) :
                      {Bool.and(_, Bool.not(B.at(Bool, False{}, s, p))) == True{} : Bool};
                    P.and_true_r(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, s, p)), sf),
                  %Equal.sym(Maybe<&2, T.Pos>, G.first_safe(layout, s, G.safe_list(w, h, s, k)), Some{p}, fe) :
                    {G.assist.safe(_, g0) == G.open(g0, p) : G.Game};
                  {==})))

Uses (35):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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/LAWS.bend&name=hidden
  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/board.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=on_board
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=assist.safe
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=first_safe
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=knowledge
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=open
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=safe_list
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=unrevealed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=SafeAt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_assist.bend&name=on_list
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=and_true_l
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=and_true_r
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=not_true
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=WH
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_member
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=onb
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=mine_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_grid.bend&name=know_hidden
  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
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Status