Wide.split_cons: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide
Lines 110-112 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend&start_line=110&end_line=112

import Base

def split_cons(-n: Nat, -m: Nat, h: Bool, parts: Parts<n, m>) -> Parts<1n+n, m>:
  Split{low, high} = parts
  Split{WCon{h, low}, high}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=Parts