Quick fixes

[valis]

Implement various quick fixes:

• [x] All errors with WARNING_UNUSED level -- remove some part of the expression

• [x] ArgumentExplicitnessError -- make explicit/implicit

• [x] InstanceInferenceError (without classifying fields) -- add local instance

• [x] InstanceInferenceError (with classifying fields for local classifying expression) -- replace local parameter with a local instance; add local instance

• [x] InstanceInferenceError (with classifying fields for global classifying expression) -- search for global instances and add an import/open command

• [x] ArgInferenceError (with candidates) -- substitute a candidate

• [x] SquashedDataError -- replace \case with \scase and \func with \sfunc (or \lemma if the level is \Prop).

• [ ] CertainTypecheckingError(TRUNCATED_WITHOUT_UNIVERSE) -- add universe (max_{con \in constructors}(number of pattern matchings on I in con) - 1)

• [x] remove \truncated keyword

• [x] FieldDependencyError -- implement the field

• [ ] CertainTypecheckingError(CASE_RESULT_TYPE) -- add \return keyword (maybe with a type)

• [x] ImplicitLambdaError -- make parameter explicit; remove parameter

• [x] DefinitionArgInferenceError, FunctionArgInferenceError -- add {} or replace _ with ()

• [ ] CertainTypecheckingError(LEMMA_LEVEL,PROPERTY_LEVEL) -- add \level; make function/field

• [x] DataUniverseError -- add \truncated; remove specified universe; replace with actual universe

• [ ] ReplacementError -- add the expression from the error as a type of a \case argument or as a \case result type

• [ ] DuplicateOpenedNameError -- hide definitions

• [x] ElimSubstError -- add bindings to \case

• [ ] MissingArgumentsError -- add required number of {?}