Function lemma_refined_serializer_congruence 

pub broadcast proof fn lemma_refined_serializer_congruence<A, B, P1, P2>(
    a: Refined<A, P1>,
    b: Refined<B, P2>,
)
where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    P1: SpecPred<A::Val>,
    P2: SpecPred<A::Val>,

requires

serializer_congruent(a.0, b.0),

forall |v: A::Val| #[trigger] a.1.apply(v) <==> b.1.apply(v),

ensures

#[trigger] serializer_congruent(a, b),