Function Uninhabited 

pub open spec fn Uninhabited<Tag>() -> VoidTag<Tag>

{ VoidTag(core::marker::PhantomData) }

Convenience constructor for VoidTag.