law view_length

lawful-arrays@0.1.0.0 · proof_tree.bend:151

import Base
import lawful-arrays@0.1.0.0/defs.bend as D

151law view_length:
152  for -T: Data
153  for +d: Nat
154  for +t: Tree<T>
155  for +hf: {D.full(T, fromT(T, t), d) == True{} : Bool}
156  {List.length(&2, T, D.view(T, fromT(T, t))) == Nat.pow(2n, d) : Nat}