Function lemma_sum_parser_congruence 

pub broadcast proof fn lemma_sum_parser_congruence<A1: SpecParser, A2: SpecParser<PVal = A1::PVal>, B1: SpecParser, B2: SpecParser<PVal = B1::PVal>>(
    a: Sum<A1, B1>,
    b: Sum<A2, B2>,
)

requires

match (a, b) {
    (Sum::Inl(a), Sum::Inl(b)) => parser_congruent(a, b),
    (Sum::Inr(a), Sum::Inr(b)) => parser_congruent(a, b),
    _ => false,
},

ensures

#[trigger] parser_congruent(a, b),