def lift_push

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake3/tree.bend:105

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

105def lift_push(+t: K.Stack, +c: T.CV) -> {lift(K.push(t,c)) == K.SEmpty{K.push(t,c)} : K.Stack}:
106  match t:
107    case K.StkNil{}: {==}
108    case K.SEmpty{+r}: {==}
109    case K.SFull{+d,+r}: {==}