ProofFlood.at_true_self.col: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_flood.bend as ProofFlood
Lines 18-30 of minebender-game@1.0.0.0/proof_flood.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_flood.bend&start_line=18&end_line=30

import Base
import minebender-game@1.0.0.0/proof_base.bend as P
import minebender-game@1.0.0.0/proof_lists.bend as PL

def at_true_self.col(+r: List<&2, Bool>, +x: Nat, +b: Bool,
  be: {Nat.is_lt(x, List.length(&2, Bool, r)) == b : Bool},
  e: {Maybe.default(&2, Bool, List.get(&2, Bool, r, x), False{}) == True{} : Bool}) ->
  {Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool}:
  match b:
    case True{}:
      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), Some{True{}},
        PL.get_set_eq(Bool, r, x, True{}, be)) : {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}
      {==}
    case False{}:
      Empty.absurd({Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool},
        P.false_ne_true(%P.get_out(Bool, r, x, be) :
          {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; e))

Uses (14):
  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=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.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.set
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.default
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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_base.bend&name=get_out
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=get_set_eq