Function lemma_repeat_n_spec_parse_congruence 

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

requires

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

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

ensures

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