law row_true_sum

minebender-game@1.0.0.0 · proof_solver.bend:70

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

70law row_true_sum:
71  for +r: List<&2, Maybe<&2, Bool>>
72  {S.row_true(r) == PU.rsum(~Maybe<&2, Bool>, ~tf, r) : Nat}