Function lemma_repeat_n_prepare_congruence 

pub broadcast proof fn lemma_repeat_n_prepare_congruence<A, B, N1, N2>(
    a: RepeatN<A, N1>,
    b: RepeatN<B, N2>,
)
where
    A: Consistency + SpecByteLen<T = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val>,
    N1: AsLen,
    N2: AsLen,

requires

prepare_congruent(a.1, b.1),

a.0.as_nat() == b.0.as_nat(),

ensures

#[trigger] prepare_congruent(a, b),