law rep_default

minebender-game@1.0.0.0 · proof_lists.bend:431

import Base

431law rep_default:
432  for -A: Data
433  for +n: Nat
434  for +v: A
435  for +i: Nat
436  {Maybe.default(&2, A, List.get(&2, A, List.replicate(A, n, v), i), v) == v : A}