def init_snoc

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:277

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

277def init_snoc(-A: Data, +xs: List<&2, A>, +x: A) -> {SC.init(A, SC.snoc(A, xs, x)) == xs : List<&2, A>}:
278  match xs:
279    case Nil{}:
280      {==}
281    case Con{h, Nil{}}:
282      {==}
283    case Con{+h, Con{+h2, +t2}}:
284      cons_cong(A, h, SC.init(A, SC.snoc(A, Con{h2, t2}, x)), Con{h2, t2}, init_snoc(A, Con{h2, t2}, x))