Function lemma_cond_prepare_congruence

Source

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

Expand description

requires

a.0 == b.0,

prepare_congruent(a.1, b.1),

ensures

#[trigger] prepare_congruent(a, b),

lemma_cond_prepare_congruence

Function lemma_cond_prepare_congruence Copy item path

Function lemma_cond_prepare_congruence