remove commented-out axioms; fix weakest-pre and also change it to no longer contain the final view shift; re-establish adequacy

construct a CMRAExt for Agreement. This completes the CMRAExt for the final world, which completes the entire construction - it's all admit-free! :-))

However, there's still a bad admit left in iris_core...