feat(builtin/kernel): add another rewrite rule

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/kernel.lean

@@ -349,6 +349,9 @@ theorem imp_falser (a : Bool) : (a → false) ↔ ¬ a
 theorem imp_falsel (a : Bool) : (false → a) ↔ true
 := case (λ x, (false → x) ↔ true) trivial trivial a
 
+theorem imp_id (a : Bool) : (a → a) ↔ true
+:= eqt_intro (λ H : a, H)
+
 theorem imp_or (a b : Bool) : (a → b) ↔ ¬ a ∨ b
 := iff_intro
      (assume H : a → b,

src/kernel/kernel_decls.cpp

@@ -100,6 +100,7 @@ MK_CONSTANT(imp_truer_fn, name("imp_truer"));
 MK_CONSTANT(imp_truel_fn, name("imp_truel"));
 MK_CONSTANT(imp_falser_fn, name("imp_falser"));
 MK_CONSTANT(imp_falsel_fn, name("imp_falsel"));
+MK_CONSTANT(imp_id_fn, name("imp_id"));
 MK_CONSTANT(imp_or_fn, name("imp_or"));
 MK_CONSTANT(not_true, name("not_true"));
 MK_CONSTANT(not_false, name("not_false"));

src/kernel/kernel_decls.h

@@ -293,6 +293,9 @@ inline expr mk_imp_falser_th(expr const & e1) { return mk_app({mk_imp_falser_fn(
 expr mk_imp_falsel_fn();
 bool is_imp_falsel_fn(expr const & e);
 inline expr mk_imp_falsel_th(expr const & e1) { return mk_app({mk_imp_falsel_fn(), e1}); }
+expr mk_imp_id_fn();
+bool is_imp_id_fn(expr const & e);
+inline expr mk_imp_id_th(expr const & e1) { return mk_app({mk_imp_id_fn(), e1}); }
 expr mk_imp_or_fn();
 bool is_imp_or_fn(expr const & e);
 inline expr mk_imp_or_th(expr const & e1, expr const & e2) { return mk_app({mk_imp_or_fn(), e1, e2}); }