VScode wishlist

• Turn current goal into lemma Done by extract_goal.
• Help with naming conventions
• Help with formatting
• Translate between tactic and term-mode proofs
• After typing identifier, insert the correct number of _s based on the number of explicit arguments to the function
• Hotkey switches to @-identifier and inserts _s in the correct places
• Editor tells you if you have written a rfl lemma and it inserts the proof for you