Function lemma_prepare_congruent_intro 

pub broadcast proof fn lemma_prepare_congruent_intro<A, B>(a: A, b: B)
where
    A: Consistency + SpecByteLen<T = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val>,

requires

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

forall |v: A::Val| #[trigger] a.byte_len(v) == b.byte_len(v),

ensures

#[trigger] prepare_congruent(a, b),