Function lemma_const_parser_congruence 

pub broadcast proof fn lemma_const_parser_congruence<Inner1: SpecParser<PVal = T>, Inner2: SpecParser<PVal = T>, T>(
    a: Const<Inner1, T>,
    b: Const<Inner2, T>,
)

requires

parser_congruent(a.0, b.0),

a.1 == b.1,

ensures

#[trigger] parser_congruent(a, b),