Function lemma_repeat_n_parse_n_rec_congruence 

pub proof fn lemma_repeat_n_parse_n_rec_congruence<A: SpecParser, B: SpecParser<PVal = A::PVal>, N: AsLen>(
    a: &RepeatN<A, N>,
    b: &RepeatN<B, N>,
    count: nat,
    ibuf: Seq<u8>,
)

requires

forall |x: Seq<u8>| #[trigger] a.1.spec_parse(x) == b.1.spec_parse(x),

ensures

a.parse_n_rec(count, ibuf) == b.parse_n_rec(count, ibuf),