feat(frontends/lean/placeholder_elaborator): add 'elaborator.unique_class_instances' flag, closes #265

By default, it is false.
When it is true, class instance resolution generates an error if there
is more than one solution.
feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution
feat(frontends/lean): make `set_option` affect fingerprints
test(tests/lean): add unique class instance resolution test