Function lemma_repeat_till_end_parser_congruence 

pub broadcast proof fn lemma_repeat_till_end_parser_congruence<A: SpecParser, B: SpecParser<PVal = A::PVal>>(
    a: A,
    b: B,
)

requires

parser_congruent(a, b),

ensures

#[trigger] parser_congruent(RepeatTillEnd(a), RepeatTillEnd(b)),