Function lemma_repeat_parser_congruence 

pub broadcast proof fn lemma_repeat_parser_congruence<A: SpecParser, B: SpecParser<PVal = A::PVal>, T1: SpecParser, T2: SpecParser<PVal = T1::PVal>>(
    a: A,
    b: B,
    t1: T1,
    t2: T2,
)

requires

parser_congruent(a, b),

parser_congruent(t1, t2),

ensures

#[trigger] parser_congruent(Repeat(a, t1), Repeat(b, t2)),