Function lemma_prepare_congruent_byte_len

Source

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

Expand description

requires

prepare_congruent(a, b),

ensures

#[trigger] a.byte_len(v) == #[trigger] b.byte_len(v),

lemma_prepare_congruent_byte_len

Function lemma_prepare_congruent_byte_len Copy item path

Function lemma_prepare_congruent_byte_len