Theorem: SciLean.val_erase (SciLean/Util/RunTimeErased.lean)

State before:
α : Sort u_1
a : α
⊢ RunTimeErased.val (erase a) = a
Tactic:
sorry_proof
State after:
no goals