Skip to main content

lemma_cond_serializer_congruence

vest_lib::combinators::congruence

Function lemma_cond_serializer_congruence 

Source 
pub broadcast proof fn lemma_cond_serializer_congruence<A, B>(a: Cond<A>, b: Cond<B>)
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.0 == b.0,
serializer_congruent(a.1, b.1),
ensures
#[trigger] serializer_congruent(a, b),