Function lemma_mapped_spec_parse_congruence 

pub proof fn lemma_mapped_spec_parse_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

forall |x: Seq<u8>| #[trigger] inner1.spec_parse(x) == inner2.spec_parse(x),

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

ensures

forall |x: Seq<u8>| {
    #[trigger]
    (Mapped {
        inner: inner1,
        mapper: mapper1,
    })
        .spec_parse(x)
        == (Mapped {
            inner: inner2,
            mapper: mapper2,
        })
            .spec_parse(x)
},