Function axiom_string_borrow 

pub broadcast proof fn axiom_string_borrow(s: &String)

ensures

#[trigger] <String as BorrowSpec<str>>::borrow_spec(s)@ == s@,