@mei@donotsta.re @zwarich@hachyderm.io A crucial ingredient of this proof is large elimination of accessibility (in fact, we do know that CIC is weaker than ZFC without large elim of accessibility). Unfortunately, this ingredient does not play nicely with the standard double-negation translation, because we do not have a large eliminator for ¬¬Acc.