Function lemma_bind_prepare_congruence 

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

requires

prepare_congruent(a.0, b.0),

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

ensures

#[trigger] prepare_congruent(a, b),