refactor(library/tactic): remove cex_builder and 'precision' for proof_state's

These two features make sense for solvers, but not in a general purpose tactic framework for building proofs like the one in Lean.

In most cases, we cannot build a counterexample anyway. These two features should be added in a custom framework for combining preprocessing techniques like in Z3.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(kernel): store binder_infor in local constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/standard): add copyright to library files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add function extensionality axiom

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add equal_f theorem

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/converter): missing case for local constants

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/inductive): bug in inductive datatype computational rule, we *must* first instantiate universe variables, *and then* the arguments

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): define heq, and configure 'calc' for '='

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean): reduce code duplication

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(frontends/lean/parser): move parser Lua bindings to a separate file

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean/inductive_cmd): cleanup

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(frontends/lean/inductive_cmd): cleanup