Function lemma_const_serializer_congruence

Source

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

Expand description

requires

a.1 == b.1,

serializer_congruent(a.0, b.0),

ensures

#[trigger] serializer_congruent(a, b),

lemma_const_serializer_congruence

Function lemma_const_serializer_congruence Copy item path

Function lemma_const_serializer_congruence