See the docs for [intuition](https://coq.inria.fr/refman/proofs/automatic-tactics/logic.html#coq:tacn.intuition). Often, `intuition idtac` will work.
See the docs for intuition. Often,
intuition idtacwill work.