Function lemma_mapped_parser_congruence 

pub broadcast proof fn lemma_mapped_parser_congruence<Inner1: SpecParser, Inner2: SpecParser<PVal = Inner1::PVal>, M1: SpecMapper<In = Inner1::PVal>, M2: SpecMapper<In = Inner2::PVal, Out = M1::Out>>(
    inner1: Inner1,
    inner2: Inner2,
    mapper1: M1,
    mapper2: M2,
)

requires

parser_congruent(inner1, inner2),

forall |v: Inner1::PVal| #[trigger] mapper1.spec_map(v) == mapper2.spec_map(v),

ensures

#[trigger]
parser_congruent(
    Mapped {
        inner: inner1,
        mapper: mapper1,
    },
    Mapped {
        inner: inner2,
        mapper: mapper2,
    },
),