Function axiom_new_strlit_view_id 

pub broadcast proof fn axiom_new_strlit_view_id(id: int)

ensures

strlit_view_id(#[trigger] strslice_new_strlit(id).view()) == id,

Distinct string literals have provably distinct views.