Function to_string_from_display_ensures Copy item path

pub uninterp spec fn to_string_from_display_ensures<T: Display + ?Sized>(
    t: &T,
    s: String,
) -> bool