Function lemma_bind_serializer_congruence 

pub broadcast proof fn lemma_bind_serializer_congruence<A1, A2, B1, B2>(
    a: Bind<A1, B1>,
    b: Bind<A2, B2>,
)
where
    A1: Consistency + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    A2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    B1: SpecMap<Input = A1::Val>,
    B2: SpecMap<Input = A1::Val>,
    B1::Output: Consistency + SpecByteLen<T = <B1::Output as Consistency>::Val> + SpecSerializer<SVal = <B1::Output as Consistency>::Val>,
    B2::Output: Consistency<Val = <B1::Output as Consistency>::Val> + SpecByteLen<T = <B1::Output as Consistency>::Val> + SpecSerializer<SVal = <B1::Output as Consistency>::Val>,

requires

serializer_congruent(a.0, b.0),

forall |key: A1::Val| {
    #[trigger]
    serializer_congruent(a.1.spec_map(key), b.1.spec_map(key))
},

ensures

#[trigger] serializer_congruent(a, b),