Tracker for HOL features merged to master

[mezpusz]

General:

• HOL unification
• HOL matching
• SMTLIB2 parsing for lambdas and applications.

Preprocessing:

• CNF
• Function definition elimination
• Proxy axioms
• Heuristic instantiations?

Inferences:

• ArgCong
• BetaEtaISE
• BoolEqToDiseq
• BoolSimp
• Cases
• CasesSimp
• Choice
• LazyClausification
• LazyClausificationGIE
• EagerClausificationISE
• IFFXORRewriterISE
• ElimLeibniz
• FlexFlexSimplify
• Injectivity
• NegativeExt
• PositiveExt
• PrimitiveInstantiation
• ImitateProject?

Inferences that need adjusting:

• Superposition
• Demodulation
• Subsumption
• Definition introduction

Which inferences are incompatible with HOL?
Proof checking for HOL?

Issues:

• Fix order of arguments for app, arrowSort, lambda calls and scrutinize every call site.
• Consider replacing EqHelper::replace with SubtermReplacer that can shift DB indices if needed.
• Make all binders compatible with HO matching (no loose DB indices can be bound).