Function lemma_optional_parser_congruence 

pub broadcast proof fn lemma_optional_parser_congruence<A1: SpecParser, A2: SpecParser<PVal = A1::PVal>, B1: SpecParser, B2: SpecParser<PVal = B1::PVal>>(
    a1: A1,
    a2: A2,
    b1: B1,
    b2: B2,
)

requires

parser_congruent(a1, a2),

parser_congruent(b1, b2),

ensures

#[trigger] parser_congruent(Optional(a1, b1), Optional(a2, b2)),