def off.llen_app

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

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

1038def off.llen_app(a: List<&2, U32>, +b: List<&2, U32>) -> {B.len(B.append(a, b)) == Nat.add(B.len(a), B.len(b)) : Nat}:
1039  match a:
1040    case Nil{}:
1041      {==}
1042    case Con{h, t}:
1043      Equal.cong(Nat, Nat, k => 1n+k, B.len(B.append(t, b)), Nat.add(B.len(t), B.len(b)), off.llen_app(t, b))