@AlgoCompSynth The paper doesn’t say — but Rocq type checking is deterministic and cheap — they aren’t running a SAT solver or anything.