Function lemma_agree Copy item path

pub proof fn lemma_agree<T>(tracked 
    a: &Resource<AgreementRA<T>>,
tracked     b: &Resource<AgreementRA<T>>,
)

a.loc() == b.loc(),

a.value()@ == b.value()@,