Function vstd::std_specs::control_flow::spec_from_blanket_identity

source · 
pub broadcast proof fn spec_from_blanket_identity<T>(t: T, s: T)
Expand description
ensures
#[trigger] spec_from::<T, T>(t, s) ==> t == s,