PROOF.tr.len_go: def of bend-osdev-mode-core@0.1.0.0
Import: import bend-osdev-mode-core@0.1.0.0/PROOF.bend as PROOF
Lines 506-511 of bend-osdev-mode-core@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-mode-core@0.1.0.0/PROOF.bend&start_line=506&end_line=511

import Base
import bend-osdev-mode-core@0.1.0.0/mode_core.bend as M
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

def tr.len_go(+bs: List<&2, M.CmBlock>, +n: Nat) -> {M.cm.blocks.len.go(bs, n) == Nat.add(List.length(&2, M.CmBlock, bs), n) : Nat}:
  match bs:
    case Nil{}:
      {==}
    case Con{h, t}:
      Equal.trans(Nat, M.cm.blocks.len.go(t, 1n+n), Nat.add(List.length(&2, M.CmBlock, t), 1n+n), 1n+Nat.add(List.length(&2, M.CmBlock, t), n), tr.len_go(t, 1n+n), UL.nat_add_succ(List.length(&2, M.CmBlock, t), n))

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=CmBlock
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-mode-core@0.1.0.0/mode_core.bend&name=cm.blocks.len.go
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_succ