Model.Integer: type of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend as Model
Lines 3-6 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend&start_line=3&end_line=6

import Base

# Negative{n} denotes -(n+1), so zero has exactly one representation.
type Integer is Data:
  Positive{magnitude: Nat}
  Negative{predecessor: Nat}

Uses (1):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat