fix(emacs/lean-mode): add comment-start "--"

fix #113
chore(frontends/lean/inductive_cmd): add auxiliary assertion for debugging

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/logic): move identities from classical to identities
fix(library): rename congr class to congruence