ProofSolver.tcontains_pre: law of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 2585-2590 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=2585&end_line=2590

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S

law tcontains_pre:
  for +pre: List<&2, S.Todo>
  for +base: List<&2, S.Todo>
  for +q: T.Pos
  for e: {tcontains(base, q) == True{} : Bool}
  {tcontains(List.append(&2, S.Todo, pre, base), q) == True{} : Bool}

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.append
  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_cells.bend&name=or_true_r
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=tcontains
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Todo
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos