Function lemma_cond_parser_congruence 

pub broadcast proof fn lemma_cond_parser_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>>(
    a: Cond<Inner1>,
    b: Cond<Inner2>,
)

requires

a.0 == b.0,

parser_congruent(a.1, b.1),

ensures

#[trigger] parser_congruent(a, b),