law rsum_at_shift

minebender-game@1.0.0.0 · proof_sums.bend:180

import Base

180law rsum_at_shift:
181  for ~A: Data
182  for ~f: A -> Nat
183  for +d: A
184  for +a: A
185  for +t: List<&2, A>
186  for +xs: List<&2, Nat>
187  {rsum_at(~A, ~f, d, a <> t, smap(xs)) == rsum_at(~A, ~f, d, t, xs) : Nat}