law row_true_set_t

minebender-game@1.0.0.0 · proof_speed.bend:38

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

38law row_true_set_t:
39  for +r: List<&2, Maybe<&2, Bool>>
40  for +x: Nat
41  for e: {List.get(&2, Maybe<&2, Bool>, r, x) == Some{None{}} : Maybe<&2, Maybe<&2, Bool>>}
42  {S.row_true(List.set(&2, Maybe<&2, Bool>, r, x, Some{True{}})) == 1n+S.row_true(r) : Nat}