proofs
Provedalphaalpha-core-v0erasurequantitative-types

Alpha Core v0: erasure removes the erased type argument from the fixture

erase⁡([],fixture⁡)=some⁡(runtimeFixture⁡)\htmlData{mx=3}{\htmlData{mx=0}{\operatorname{erase}}(\htmlData{mx=1}{\left[ \right]}, \htmlData{mx=2}{\operatorname{fixture}})} \mathrel{\htmlData{mx=7}{=}} \htmlData{mx=6}{\htmlData{mx=4}{\operatorname{some}}(\htmlData{mx=5}{\operatorname{runtimeFixture}})}
What the notation means · or point at any symbol
erase
erase: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (erase)
f(x)Function application
erase applied to [], fixture. Lean writes f x; papers write f(x). (erase [] fixture)
=Equality
erase([], fixture) and some(runtimeFixture) are the same. (erase [] fixture = some runtimeFixture)
[a, b]List
The list of , in order. ([])
fixture
fixture: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (fixture)
some
some: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (some)
runtimeFixture
runtimeFixture: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (runtimeFixture)

Erasing the fixture drops the identity's erased (quantity 0) binder and its Nat argument, leaving the runtime term (λ¹ value. value) (successor zero).

How it was proved

Proved
21 October 2026
By
Ajax
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
7 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements