ProofGrid.contains_remove_other.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_grid.bend as ProofGrid
Lines 258-279 of minebender-game@1.0.0.0/proof_grid.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_grid.bend&start_line=258&end_line=279

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B

def contains_remove_other.go(+e0: T.Pos, +t: List<&2, T.Pos>, +p: T.Pos, +q: T.Pos,
  d: {B.same(p, q) == False{} : Bool}, +b: Bool, +e: {B.same(e0, p) == b : Bool},
  ih: {B.contains(B.remove(t, p), q) == B.contains(t, q) : Bool}) ->
  {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(B.same(e0, p))), q)
    == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}:
  match b:
    case True{}:
      %Equal.sym(Bool, B.same(e0, p), True{}, e) :
        {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(_)), q)
          == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}
      %Equal.sym(T.Pos, e0, p, same_sound(e0, p, e)) :
        {B.contains(B.remove(t, p), q) == Bool.or(B.same(_, q), B.contains(t, q)) : Bool}
      %Equal.sym(Bool, B.same(p, q), False{}, d) :
        {B.contains(B.remove(t, p), q) == Bool.or(_, B.contains(t, q)) : Bool}
      ih
    case False{}:
      %Equal.sym(Bool, B.same(e0, p), False{}, e) :
        {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(_)), q)
          == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}
      %ih : {Bool.or(B.same(e0, q), B.contains(B.remove(t, p), q))
        == Bool.or(B.same(e0, q), _) : Bool}
      {==}

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=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.filter.put
  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=remove
  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_sound
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos