ProofCells.allp_member: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_cells.bend as ProofCells
Lines 38-47 of minebender-game@1.0.0.0/proof_cells.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_cells.bend&start_line=38&end_line=47

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/proof_base.bend as P

# A cell of a list whose cells all pass f passes f.
def allp_member(~E: Data, ~f: E -> T.Pos -> Bool, +e: E, ps: List<&2, T.Pos>, +q: T.Pos,
  +h: {allp(~E, ~f, e, ps) == True{} : Bool}, m: {B.contains(ps, q) == True{} : Bool}) ->
  {f(e, q) == True{} : Bool}:
  match ps:
    case Nil{}:
      Empty.absurd({f(e, q) == True{} : Bool}, P.false_ne_true(m))
    case +p <> +t:
      allp_member.go(~E, ~f, e, p, t, q, allp_head(~E, ~f, e, p, t, h), B.same(p, q), {==}, m,
        mt => allp_member(~E, ~f, e, t, q, allp_tail(~E, ~f, e, p, t, h), mt))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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_base.bend&name=false_ne_true
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_head
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_member.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp_tail
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos