Function lemma_repeat_prepare_congruence

Source

pub broadcast proof fn lemma_repeat_prepare_congruence<A1, A2, B1, B2>(
    a: Repeat<A1, B1>,
    b: Repeat<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>,

Expand description

requires

prepare_congruent(a.0, b.0),

prepare_congruent(a.1, b.1),

ensures

#[trigger] prepare_congruent(a, b),

lemma_repeat_prepare_congruence

Function lemma_repeat_prepare_congruence Copy item path

Function lemma_repeat_prepare_congruence