Function lemma_array_serializer_congruence 

pub broadcast proof fn lemma_array_serializer_congruence<A, B, const N: usize>(
    a: Array<N, A>,
    b: Array<N, B>,
)
where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,

requires

serializer_congruent(a.0, b.0),

ensures

#[trigger] serializer_congruent(a, b),