def append_nil

bend-osdev-crypto@0.1.0.0 · PROOF.bend:468

import bend-osdev-crypto@0.1.0.0/PROOF.bend as PROOF

import Base

468def append_nil(xs: List<&2, U32>) -> {xs == List.append(&2, U32, xs, Nil{}) : List<&2, U32>}:
469  match xs:
470    case Nil{}:
471      {==}
472    case Con{h, t}:
473      %append_nil(t) : {Con{h, t} == Con{h, _} : List<&2, U32>}
474      {==}

Uses (3)

Used by (3)