ProofLists.at_set_ne.row: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_lists.bend as ProofLists
Lines 267-287 of minebender-game@1.0.0.0/proof_lists.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_lists.bend&start_line=267&end_line=287

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 at_set_ne.row(-A: Data, +g: T.Grid(A), +x: Nat, +y: Nat, +qx: Nat, +v: A, +d: A,
  xne: {Nat.is_eq(x, qx) == False{} : Bool}, +c: Bool,
  ce: {Nat.is_lt(y, List.length(&2, List<&2, A>, g)) == c : Bool}) ->
  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, y}) == B.at(A, d, g, T.Pos{qx, y}) : A}:
  match c:
    case True{}:
      +row = row_of(A, g, y)
      +r2 = List.set(&2, A, row, x, v)
      %Equal.sym(Maybe<&2, List<&2, A>>, List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, r2), y),
        Some{r2}, get_set_eq(List<&2, A>, g, y, r2, ce)) :
        {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), qx), d)
          == B.at(A, d, g, T.Pos{qx, y}) : A}
      %Equal.sym(Maybe<&2, A>, List.get(&2, A, r2, qx), List.get(&2, A, row, qx),
        get_set_ne(A, row, x, qx, v, xne)) :
        {Maybe.default(&2, A, _, d) == B.at(A, d, g, T.Pos{qx, y}) : A}
      {==}
    case False{}:
      +r2 = List.set(&2, A, row_of(A, g, y), x, v)
      %Equal.sym(T.Grid(A), List.set(&2, List<&2, A>, g, y, r2), g, set_out(List<&2, A>, g, y, r2, ce)) :
        {B.at(A, d, _, T.Pos{qx, y}) == B.at(A, d, g, T.Pos{qx, y}) : A}
      {==}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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_eq
  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_lists.bend&name=get_set_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=get_set_ne
  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/proof_lists.bend&name=set_out
  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