ProofAssist.first_safe.lift: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_assist.bend as ProofAssist
Lines 35-50 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=35&end_line=50

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/proof_solver.bend as PV

def first_safe.lift(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +q: T.Pos, +t: List<&2, T.Pos>,
  r: SafeAt(layout, shown, t), -hit: Bool, he: {hit == False{} : Bool}) ->
  Exists(T.Pos, p => {G.first_safe.go(q <> t, hit, layout, shown) == Some{p} : Maybe<&2, T.Pos>} &
    ({Bool.and(Bool.not(B.mine(layout, p)), Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool} &
     {B.contains(q <> t, p) == True{} : Bool})):
  match r:
    case (+p, pr):
      match pr:
        case (fe, rest):
          match rest:
            case (sf, m):
              %Equal.sym(Bool, hit, False{}, he) :
                Exists(T.Pos, p2 => {G.first_safe.go(q <> t, _, layout, shown) == Some{p2} : Maybe<&2, T.Pos>} &
                  ({Bool.and(Bool.not(B.mine(layout, p2)), Bool.not(B.at(Bool, False{}, shown, p2))) == True{} : Bool} &
                   {B.contains(q <> t, p2) == True{} : Bool}))
              (p, (fe, (sf, PV.or_r(B.same(q, p), B.contains(t, p), m))))

Uses (18):
  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=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=at
  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=mine
  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/game.bend&name=first_safe.go
  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_solver.bend&name=or_r
  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