Skip to main content

lemma_prepare_congruent_transitive

vest_lib::combinators::congruence

Function lemma_prepare_congruent_transitive 

Source 
pub proof fn lemma_prepare_congruent_transitive<A, B, C>(a: A, b: B, c: C)
where
    A: Consistency + SpecByteLen<T = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val>,
    C: Consistency<Val = A::Val> + SpecByteLen<T = A::Val>,
Expand description
requires
prepare_congruent(a, b),
prepare_congruent(b, c),
ensures
prepare_congruent(a, c),