Not sure if it's what you're asking for, but in lean, you can put `sorry` to skip a proof. It's `believe_me` in Idris2, and I think the Agda version is `trustMe`.
You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).
You can also use stuff like ! when you don't want to prove your array indices (it might crash or substitute a dummy value if you're wrong).