The Erased struct witnesses the logical ownership of a value of type T while remaining zero-sized. This can be used for ghost proofs of soundness.
The Exists trait is intended to be used with
impl, to denote
an argument where the existence of a value is sufficient as an argument
T implements SingleThread if at any time there
is a single thread from which all values/references to
values of this type may be accessed.
This trait denotes a type which has at most one logical identity at all times. This is sufficient to make borrowing decisions based only on the type, without regards to value identity.