Function lemma_mapped_serializer_congruence 

pub broadcast proof fn lemma_mapped_serializer_congruence<A, B, M1, M2>(
    a: Mapped<A, M1>,
    b: Mapped<B, M2>,
)
where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    M1: SpecMapper<In = A::Val>,
    M2: SpecMapper<In = A::Val, Out = M1::Out>,

requires

serializer_congruent(a.inner, b.inner),

forall |v: M1::Out| #[trigger] a.mapper.spec_map_rev(v) == b.mapper.spec_map_rev(v),

forall |v: M1::Out| #[trigger] a.mapper.wf_out(v) <==> b.mapper.wf_out(v),

ensures

#[trigger] serializer_congruent(a, b),