Tools: Rocq (formerly Coq)
INFO
(Language feature/design, Formal system, Proof/Reason technique) A proof Command in Rocq that transforms the current Goal state, automating proof steps (like intros, apply, rewrite) to incrementally construct a proof term.