def app_nil8

bend-osdev-bytes@0.1.1.0 · PROOF.bend:241

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

241def app_nil8(+ws: List<&2, B.OctByte>) -> {List.append(&2, B.OctByte, ws, Nil{}) == ws : List<&2, B.OctByte>}:
242  match ws:
243    case Nil{}:
244      {==}
245    case Con{h, t}:
246      Equal.cong(List<&2, B.OctByte>, List<&2, B.OctByte>, l => Con{h, l}, List.append(&2, B.OctByte, t, Nil{}), t, app_nil8(t))