List.init_snoc: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as List
Lines 277-284 of bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend&start_line=277&end_line=284

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

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

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend&name=cons_cong
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=init
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=snoc