Function no_lookahead_parser 

pub open spec fn no_lookahead_parser<T>(parser: ParserFnSpec<T>) -> bool

{
    forall |i1: Seq<u8>, i2: Seq<u8>| {
        (#[trigger]
        parser(
            i1,
        ) matches Some(
            (n, v),
        ) ==> 0 <= n <= i2.len()
            ==> (i2.take(n) == i1.take(n) ==> #[trigger] parser(i2) == Some((n, v))))
    }
}

Functional version of NoLookAhead for parsers.