law list_len_append

bend-osdev-mode-core@0.1.0.0 · LAWS.bend:57

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

57law list_len_append:
58  for +a: List<&2, U32>
59  for +b: List<&2, U32>
60  {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}