Coq induction support in proof mode
There is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.
There is no "right" way to do induction when in proof mode.
The minimal feature would be to provide a tactic to revert a proof mode goal (with empty context ?) into a standard Coq goal.