def length_snoc

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/lists.bend:68

import Base
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

68def length_snoc(-A: Data, +xs: List<&2,A>, +x: A) -> {SC.length(A,SC.append(A,xs,Con{x,Nil{}})) == 1n+SC.length(A,xs) : Nat}:
69  match xs:
70    case Nil{}: {==}
71    case Con{+a,+t}: N.succ_cong(SC.length(A,SC.append(A,t,Con{x,Nil{}})),1n+SC.length(A,t),length_snoc(A,t,x))