Proof.pow2: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/proof.bend as Proof
Lines 65-67 of bend-collections-laws-math@1.0.0.0/proofs/math/proof.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/proof.bend&start_line=65&end_line=67

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend as P2
import bend-collections-laws-math@1.0.0.0/spec/math/pow2.bend as SP

# pow2
def pow2(+d: Nat) -> SP.Pow2t.value(d):
  P2.same(d)

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/pow2/pow2.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/pow2.bend&name=Pow2t.value