Formalize Authoritative RA from SCION in terms of RA from the gobra-libs (#411)

* Formalize Authoritative RA in terms of RA from the standard lib

* only two outstanding goals

* Adapt shape of theorems

* prove extensionality

* cleanup, finish last lemma

* update comments

Author: jcp19