law octets_len_append

bend-osdev-bytes@0.1.1.0 · LAWS.bend:239

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

239law octets_len_append:
240  for +a: B.Octets
241  for +b: B.Octets
242  {B.Octets.len(B.Octets.append(a, b)) == Nat.add(B.Octets.len(a), B.Octets.len(b)) : Nat}