def length_replicate

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:46

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

46def length_replicate(-A: Data, +n: Nat, +x: A) -> {SC.length(A, SC.replicate(A, n, x)) == n : Nat}:
47  match n:
48    case 0n:
49      {==}
50    case 1n+p:
51      N.succ_cong(SC.length(A, SC.replicate(A, p, x)), p, length_replicate(A, p, x))