def li.take_append

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:197

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

197def li.take_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.take(B.len(a), B.append(a, b)) == a : List<&2, U32>}:
198  match a:
199    case Nil{}:
200      {==}
201    case Con{+h, +t}:
202      %Equal.sym(List<&2, U32>, B.take(B.len(t), B.append(t, b)), t, li.take_append(t, b)) : {Con{h, _} == Con{h, t} : List<&2, U32>}
203      {==}