def AP.size_eq
bend-osdev-array@0.1.0.1 · PROOF.bend:599
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
599def AP.size_eq(-T: Data, t: AP.Tree<T>) -> {Array.size(T, AP.build(T, t)) == (AP.build(T, t), AP.size(T, t)) : Array<T> & U32}:
600 match t:
601 case APLeaf{x}:
602 {==}
603 case APNode{xs, ys}:
604 %Equal.sym(Array<T> & U32, Array.size(T, AP.build(T, xs)), (AP.build(T, xs), AP.size(T, xs)), AP.size_eq(T, xs)) : {Array.size.node(T, AP.build(T, ys), _) == (ANode{AP.build(T, xs), AP.build(T, ys)}, U32.shl(AP.size(T, xs))) : Array<T> & U32}
605 {==}