StorageAddressBounds.shift_extent: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
Lines 16-20 of stelliferous@0.0.2.0/proofs/storage_address_bounds.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&start_line=16&end_line=20

import Base
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

def shift_extent(depth: Nat) -> {WordEncoding.shift(depth,1n) == Shape.extent(depth) : Nat}:
  match depth:
    case 0n: {==}
    case 1n+rest:
      Equal.cong(Nat,Nat,Nat.double,WordEncoding.shift(rest,1n),Shape.extent(rest),shift_extent(rest))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=extent
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=shift