diff --git a/src/HOL/Metis_Examples/Abstraction.thy b/src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy
+++ b/src/HOL/Metis_Examples/Abstraction.thy
@@ -1,174 +1,174 @@
 (*  Title:      HOL/Metis_Examples/Abstraction.thy
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     Author:     Jasmin Blanchette, TU Muenchen
 
 Example featuring Metis's support for lambda-abstractions.
 *)
 
 section \<open>Example Featuring Metis's Support for Lambda-Abstractions\<close>
 
 theory Abstraction
-imports "HOL-Library.FuncSet"
+  imports "HOL-Library.FuncSet"
 begin
 
 (* For Christoph Benzmüller *)
 lemma "x < 1 \<and> ((=) = (=)) \<Longrightarrow> ((=) = (=)) \<and> x < (2::nat)"
 by (metis nat_1_add_1 trans_less_add2)
 
-lemma "((=) ) = (\<lambda>x y. y = x)"
+lemma "(=) = (\<lambda>x y. y = x)"
 by metis
 
 consts
   monotone :: "['a => 'a, 'a set, ('a *'a)set] => bool"
   pset  :: "'a set => 'a set"
   order :: "'a set => ('a * 'a) set"
 
 lemma "a \<in> {x. P x} \<Longrightarrow> P a"
 proof -
   assume "a \<in> {x. P x}"
   thus "P a" by (metis mem_Collect_eq)
 qed
 
 lemma Collect_triv: "a \<in> {x. P x} \<Longrightarrow> P a"
 by (metis mem_Collect_eq)
 
 lemma "a \<in> {x. P x --> Q x} \<Longrightarrow> a \<in> {x. P x} \<Longrightarrow> a \<in> {x. Q x}"
 by (metis Collect_imp_eq ComplD UnE)
 
 lemma "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A \<and> b \<in> B a"
 proof -
   assume A1: "(a, b) \<in> Sigma A B"
   hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
   have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
   have "b \<in> B a" by (metis F1)
   thus "a \<in> A \<and> b \<in> B a" by (metis F2)
 qed
 
 lemma Sigma_triv: "(a, b) \<in> Sigma A B \<Longrightarrow> a \<in> A & b \<in> B a"
 by (metis SigmaD1 SigmaD2)
 
 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 by (metis (full_types, lifting) CollectD SigmaD1 SigmaD2)
 
 lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
 proof -
   assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
   hence F1: "a \<in> A" by (metis mem_Sigma_iff)
   have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
   hence "a = f b" by (metis (full_types) mem_Collect_eq)
   thus "a \<in> A \<and> a = f b" by (metis F1)
 qed
 
 lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
 by (metis Collect_mem_eq SigmaD2)
 
 lemma "(cl, f) \<in> CLF \<Longrightarrow> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) \<Longrightarrow> f \<in> pset cl"
 proof -
   assume A1: "(cl, f) \<in> CLF"
   assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
   have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
   hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis mem_Collect_eq)
   thus "f \<in> pset cl" by (metis A1)
 qed
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
 by (metis (no_types) Collect_mem_eq Sigma_triv)
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
 proof -
   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
   have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
   thus "f \<in> pset cl \<rightarrow> pset cl" by (metis mem_Collect_eq)
 qed
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 by (metis (no_types) Collect_conj_eq Int_def Sigma_triv inf_idem)
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 proof -
   assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
   have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
   hence "f \<in> Id_on cl `` pset cl" by (metis Int_commute Image_Id_on mem_Collect_eq)
   hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
   thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
 qed
 
 lemma
   "(cl, f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
    (f \<in> pset cl \<rightarrow> pset cl)  &  (monotone f (pset cl) (order cl))"
 by auto
 
 lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF \<subseteq> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 by (metis (lifting) CollectD Sigma_triv subsetD)
 
 lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) \<Longrightarrow>
    f \<in> pset cl \<inter> cl"
 by (metis (lifting) CollectD Sigma_triv)
 
 lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
 by (metis (lifting) CollectD Sigma_triv subsetD)
 
 lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) \<Longrightarrow>
    f \<in> pset cl \<rightarrow> pset cl"
 by (metis (lifting) CollectD Sigma_triv)
 
 lemma
   "(cl, f) \<in> CLF \<Longrightarrow>
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)}) \<Longrightarrow>
    (f \<in> pset cl \<rightarrow> pset cl) & (monotone f (pset cl) (order cl))"
 by auto
 
 lemma "map (\<lambda>x. (f x, g x)) xs = zip (map f xs) (map g xs)"
 apply (induct xs)
  apply (metis list.map(1) zip_Nil)
 by auto
 
 lemma
   "map (\<lambda>w. (w \<rightarrow> w, w \<times> w)) xs =
    zip (map (\<lambda>w. w \<rightarrow> w) xs) (map (\<lambda>w. w \<times> w) xs)"
 apply (induct xs)
  apply (metis list.map(1) zip_Nil)
 by auto
 
 lemma "(\<lambda>x. Suc (f x)) ` {x. even x} \<subseteq> A \<Longrightarrow> \<forall>x. even x --> Suc (f x) \<in> A"
 by (metis mem_Collect_eq image_eqI subsetD)
 
 lemma
   "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow>
    (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)"
 by (metis mem_Collect_eq imageI rev_subsetD)
 
 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)"
 by (metis (lifting) imageE)
 
 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)"
 by (metis map_prod_def map_prod_surj_on)
 
 lemma image_TimesB:
     "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)"
 by force
 
 lemma image_TimesC:
   "(\<lambda>(x, y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) =
    ((\<lambda>x. x \<rightarrow> x) ` A) \<times> ((\<lambda>y. y \<times> y) ` B)"
 by (metis image_TimesA)
 
 end
diff --git a/src/HOL/Metis_Examples/Proxies.thy b/src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy
+++ b/src/HOL/Metis_Examples/Proxies.thy
@@ -1,267 +1,267 @@
 (*  Title:      HOL/Metis_Examples/Proxies.thy
     Author:     Jasmin Blanchette, TU Muenchen
 
 Example that exercises Metis's and Sledgehammer's logical symbol proxies for
 rudimentary higher-order reasoning.
 *)
 
 section \<open>
 Example that Exercises Metis's and Sledgehammer's Logical Symbol Proxies for
 Rudimentary Higher-Order Reasoning.
 \<close>
 
 theory Proxies
 imports Type_Encodings
 begin
 
-sledgehammer_params [prover = spass, fact_filter = mepo, timeout = 30, preplay_timeout = 0,
-  dont_minimize]
+sledgehammer_params [prover = spass, fact_filter = mepo, slices = 1, timeout = 30,
+  preplay_timeout = 0, dont_minimize]
 
 text \<open>Extensionality and set constants\<close>
 
 lemma plus_1_not_0: "n + (1::nat) \<noteq> 0"
 by simp
 
 definition inc :: "nat \<Rightarrow> nat" where
 "inc x = x + 1"
 
 lemma "inc \<noteq> (\<lambda>y. 0)"
 sledgehammer [expect = some] (inc_def plus_1_not_0)
 by (metis_exhaust inc_def plus_1_not_0)
 
 lemma "inc = (\<lambda>y. y + 1)"
 sledgehammer [expect = some]
 by (metis_exhaust inc_def)
 
 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "add_swap = (\<lambda>x y. y + x)"
 
 lemma "add_swap m n = n + m"
 sledgehammer [expect = some] (add_swap_def)
 by (metis_exhaust add_swap_def)
 
 definition "A = {xs::'a list. True}"
 
 lemma "xs \<in> A"
 (* The "add:" argument is unfortunate. *)
 sledgehammer [expect = some] (add: A_def mem_Collect_eq)
 by (metis_exhaust A_def mem_Collect_eq)
 
 definition "B (y::int) \<equiv> y \<le> 0"
 definition "C (y::int) \<equiv> y \<le> 1"
 
 lemma int_le_0_imp_le_1: "x \<le> (0::int) \<Longrightarrow> x \<le> 1"
 by linarith
 
 lemma "B \<le> C"
 sledgehammer [expect = some]
 by (metis_exhaust B_def C_def int_le_0_imp_le_1 predicate1I)
 
 text \<open>Proxies for logical constants\<close>
 
 lemma "id (=) x x"
 sledgehammer [type_enc = erased, expect = none] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis (full_types) id_apply)
 
 lemma "id True"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "\<not> id False"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "x = id True \<or> x = id False"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id x = id True \<or> id x = id False"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "P True \<Longrightarrow> P False \<Longrightarrow> P x"
 sledgehammer [type_enc = erased, expect = none] ()
 sledgehammer [type_enc = poly_args, expect = none] ()
 sledgehammer [type_enc = poly_tags??, expect = some] ()
 sledgehammer [type_enc = poly_tags, expect = some] ()
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] ()
 sledgehammer [type_enc = mono_tags??, expect = some] ()
 sledgehammer [type_enc = mono_tags, expect = some] ()
 sledgehammer [type_enc = mono_guards??, expect = some] ()
 sledgehammer [type_enc = mono_guards, expect = some] ()
 by (metis (full_types))
 
 lemma "id (\<not> a) \<Longrightarrow> \<not> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> \<not> a) \<Longrightarrow> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by metis_exhaust
 
 lemma "id (\<not> (id (\<not> a))) \<Longrightarrow> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id a"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<and> b) \<Longrightarrow> id b"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id b \<Longrightarrow> id (a \<and> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id a \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id b \<Longrightarrow> id (a \<or> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (\<not> b) \<Longrightarrow> id (\<not> (a \<or> b))"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (\<not> a) \<Longrightarrow> id (a \<longrightarrow> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 lemma "id (a \<longrightarrow> b) \<longleftrightarrow> id (\<not> a \<or> b)"
 sledgehammer [type_enc = erased, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_tags, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = poly_guards, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_tags, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards??, expect = some] (id_apply)
 sledgehammer [type_enc = mono_guards, expect = some] (id_apply)
 by (metis_exhaust id_apply)
 
 end