StorageShape.unique_depth: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_shape.bend as StorageShape
Lines 81-92 of stelliferous@0.0.2.0/proofs/storage_shape.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&start_line=81&end_line=92

import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

def unique_depth(-Element: Data,tree: Tree.Tree<Element>,left_depth: Nat,right_depth: Nat,
  left: Balanced(Element,left_depth,tree),right: Balanced(Element,right_depth,tree)) -> {left_depth == right_depth : Nat}:
  match tree left_depth right_depth:
    case Tree.Leaf{value} 0n 0n: {==}
    case Tree.Leaf{value} 0n 1n+right_depth: match right:
    case Tree.Leaf{value} 1n+left_depth right_depth: match left:
    case Tree.Node{left_tree,right_tree} 0n right_depth: match left:
    case Tree.Node{left_tree,right_tree} 1n+left_depth 0n: match right:
    case Tree.Node{+left_tree,right_tree} 1n+ +left_depth 1n+ +right_depth:
      Both{left_balanced,left_other} = left
      Both{right_balanced,right_other} = right
      Equal.cong(Nat,Nat,depth => 1n+depth,left_depth,right_depth,unique_depth(Element,left_tree,left_depth,right_depth,left_balanced,right_balanced))

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=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=Both
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree