def g_lenu

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

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

500def g_lenu(+xs: List<&2, U32>, +n: Nat) -> {B.len.go(xs, n) == Nat.add(B.len(xs), n) : Nat}:
501  match xs:
502    case Nil{}:
503      {==}
504    case Con{h, t}:
505      Equal.trans(Nat, B.len.go(t, 1n+n), Nat.add(B.len(t), 1n+n), 1n+Nat.add(B.len(t), n),
506        g_lenu(t, 1n+n), UL.nat_add_succ(B.len(t), n))