Function next_post Copy item path

pub uninterp spec fn next_post<'a>(
    old_chars: &Chars<'a>,
    new_chars: &Chars<'a>,
    ret: Option<char>,
) -> bool