Erased.out_proof

theorem Erased.out_proof : ∀ {p : Prop}, Erased p → p

The theorem `Erased.out_proof` asserts that for every proposition `p`, if `p` is of the type `Erased p`, then `p` is true. In other words, if we have an erased proof of a proposition, we can extract that proof, confirming the truth of the proposition. This is useful in situations where we're working with proofs that have been erased for efficiency in the Lean virtual machine, but where we still need to ascertain the truth of the propositions they prove.

More concisely: If a proposition `p` has an erased proof in Lean, then `p` is true.