WIP: generalization to arbirary A locations, one admit

Made a gc access lemma stronger (old one was too weak for the proof)
Status Job ID Name Coverage
  Build
canceled #34855
fp-timing
build-coq.8.9.0