Function lemma_exact_len_parser_congruence 

pub broadcast proof fn lemma_exact_len_parser_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>, Len: AsLen>(
    len: Len,
    inner1: Inner1,
    inner2: Inner2,
)

requires

parser_congruent(inner1, inner2),

ensures

#[trigger] parser_congruent(ExactLen(len, inner1), ExactLen(len, inner2)),