constant-time is_ground #5
Description
rocq-prover/rocq#12600 was an issue with non-constant-time closedness checking, not evars, so we should add a requirement to be able to cache connotations that depend only on subterms (such as groundedness checking). This might be a thing that occurs off to the side rather than inside the proof engine though?