lemma_two_size_of_equal

vstd_extra::raw_ptr_extra

Function lemma_two_size_of_equal 

Source 
pub broadcast proof fn lemma_two_size_of_equal<T>()
Expand description
requires
vstd::layout::size_of::<T>() <= usize::MAX,
ensures
#[trigger] vstd::layout::size_of::<T>() == size_of::<T>(),