law new_view
import lawful-arrays@0.1.0.0/proof_tree.bend as ProofTreeimport Base
import lawful-arrays@0.1.0.0/defs.bend as D
199law new_view:
200 for -T: Data
201 for +d: Nat
202 for +v: T
203 {D.view(T, Array.new(T, d, v)) == List.replicate(T, Nat.pow(2n, d), v) : List<&2, T>}