Theorem: SciLean.erase_out (SciLean/Core/Rand/Rand.lean)

State before:
α : Sort u_1
a : α
⊢ Erased.out (erase a) = a
Tactic:
simp[erase]
State after:
no goals