Function parser_pair_some 

pub open spec fn parser_pair_some<T>(
    parser: ParserFnSpec<T>,
    buf1: Seq<u8>,
    buf2: Seq<u8>,
) -> Option<((int, T), (int, T))>

{
    match parser(buf1) {
        Some((n1, v1)) => {
            match parser(buf2) {
                Some((n2, v2)) => Some(((n1, v1), (n2, v2))),
                None => None,
            }
        }
        None => None,
    }
}