Function lemma_named_parser_congruence 

pub broadcast proof fn lemma_named_parser_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>>(
    name1: &'static str,
    name2: &'static str,
    inner1: Inner1,
    inner2: Inner2,
)

requires

parser_congruent(inner1, inner2),

ensures

#[trigger] parser_congruent(Named(name1, inner1), Named(name2, inner2)),