Function lemma_repeat_n_parser_congruence 

pub broadcast proof fn lemma_repeat_n_parser_congruence<A: SpecParser, B: SpecParser<PVal = A::PVal>, N: AsLen>(
    a: RepeatN<A, N>,
    b: RepeatN<B, N>,
)

requires

parser_congruent(a.1, b.1),

a.0.as_nat() == b.0.as_nat(),

ensures

#[trigger] parser_congruent(a, b),