I don't know if Coq with nested universes is known to be inconsistent yet, but I suppose that for this to work someone must always bankroll `inconsistent : fora

I don't know if Coq with nested universes is known to be inconsistent yet, but I suppose that for this to work someone must always bankroll `inconsistent : forall a : Set, a` at something significantly higher than any other proof on the market and the system should reject repeated proofs.