def AP.reflect.node
bend-osdev-array@0.1.0.1 · PROOF.bend:502
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
502def AP.reflect.node(-T: Data, -tx: AP.Tree<T>, -ty: AP.Tree<T>, -xs: Array<T>, -ys: Array<T>, ex: {AP.build(T, tx) == xs : Array<T>}, ey: {AP.build(T, ty) == ys : Array<T>}) -> {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{xs, ys} : Array<T>}:
503 %ex : {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{_, ys} : Array<T>}
504 %ey : {ANode{AP.build(T, tx), AP.build(T, ty)} == ANode{AP.build(T, tx), _} : Array<T>}
505 {==}