def len_init2
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/loop.bend:48
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop
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/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
48def len_init2(+r: List<&2,T.Out>, +x: T.Out) -> {SC.length(T.Out,init2(r,x)) == SC.length(T.Out,r) : Nat}:
49 match r:
50 case Nil{}: {==}
51 case Con{+y,+q}: N.succ_cong(SC.length(T.Out,init2(q,y)),SC.length(T.Out,q),len_init2(q,y))