ProofFlood.at_true_self.row: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_flood.bend as ProofFlood
Lines 32-49 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=32&end_line=49

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
import minebender-game@1.0.0.0/proof_lists.bend as PL

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

Uses (20):
  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/board.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at
  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_flood.bend&name=at_true_self.col
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=get_set_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=row_of
  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