def cvs_append
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:125
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as Tree
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as T
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as K
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as LS
125def cvs_append(+xs: List<&2,T.Out>, +ys: List<&2,T.Out>) -> {cvs(SC.append(T.Out,xs,ys)) == SC.append(T.CV,cvs(xs),cvs(ys)) : List<&2,T.CV>}:
126 match xs:
127 case Nil{}: {==}
128 case Con{+x,+r}: LS.cons_cong(T.CV,K.out_cv(x),cvs(SC.append(T.Out,r,ys)),SC.append(T.CV,cvs(r),cvs(ys)),cvs_append(r,ys))