def li.len_append

bend-osdev-mode-core@0.1.0.0 · PROOF.bend:157

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

157def li.len_append(+a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}:
158  match a:
159    case Nil{}:
160      {==}
161    case Con{+h, +t}:
162      %li.len_append(t, b) : {1n+B.len(B.append(t, b)) == 1n+_ : Nat}
163      {==}