doc(README.md): add Aquamacs case, ask to update lean-rootdir

[skip ci]
chore(emacs): remove unnecessary requires
feat(library/definitional/projection): add option for marking main premise as instance implicit (i.e., `[]` binder decorator)
feat(frontends/lean/inductive_cmd): notation for enumeration types
feat(frontends/lean/structure_cmd): checkpoint