Function lemma_ref_parser_congruence 

pub broadcast proof fn lemma_ref_parser_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>>(
    inner1: Inner1,
    inner2: Inner2,
)

requires

parser_congruent(inner1, inner2),

ensures

#[trigger] parser_congruent(Ref(inner1), Ref(inner2)),