Function lemma_sum_prepare_congruence 

pub broadcast proof fn lemma_sum_prepare_congruence<A1, A2, B1, B2>(
    a: Sum<A1, B1>,
    b: Sum<A2, B2>,
)
where
    A1: Consistency + SpecByteLen<T = A1::Val>,
    A2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val>,
    B1: Consistency + SpecByteLen<T = B1::Val>,
    B2: Consistency<Val = B1::Val> + SpecByteLen<T = B1::Val>,

requires

match (a, b) {
    (Sum::Inl(a), Sum::Inl(b)) => prepare_congruent(a, b),
    (Sum::Inr(a), Sum::Inr(b)) => prepare_congruent(a, b),
    _ => false,
},

ensures

#[trigger] prepare_congruent(a, b),