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()@,