diff --git a/src/arachne.c b/src/arachne.c
index c03add2..038557b 100644
--- a/src/arachne.c
+++ b/src/arachne.c
@@ -1615,7 +1615,7 @@ bind_goal_all_options (const Binding b)
 	{
 	  int know_only;
 
-	  know_only = 0;
+	  know_only = false;
 
 	  if (1 == 0)		// blocked for now
 	    {
@@ -1640,12 +1640,12 @@ bind_goal_all_options (const Binding b)
 			  eprintf
 			    (" is never sent from a regular run, so we only intruder construct it.\n");
 			}
-		      know_only = 1;
+		      know_only = true;
 		    }
 		}
 	    }
 
-	  if (switches.experimental & 4)
+	  if (switches.experimental & 16)
 	    {
 	      // Keylevel lemmas: improves on the previous one
 	      if (!isPossiblySent (b->term))
@@ -1665,21 +1665,33 @@ bind_goal_all_options (const Binding b)
 			}
 		      eprintf ("\n");
 		    }
-		  know_only = 1;
+		  know_only = true;
 		}
 	    }
-#ifdef DEBUG
-	  else
+
+	  if (!(switches.experimental & 32))
 	    {
-	      if (DEBUGL (5) && know_only == 1)
+		    /**
+		     * Note: this is slightly weaker than the previous & 16,
+		     * but it actually differs in such minimal cases that it
+		     * might be better to simply have the (much cleaner)
+		     * keylevel lemma.
+		     *
+		     * That's why this is default and the other isn't.
+		     */
+
+	      // Hidelevel variant
+	      int hlf;
+
+	      hlf = hidelevelFlag (sys, b->term);
+	      if (hlf == HLFLAG_NONE || hlf == HLFLAG_KNOW)
 		{
-		  eprintf
-		    ("Keylevel lemma is weaker than function lemma for term ");
-		  termPrint (b->term);
-		  eprintf ("\n");
+		  know_only = true;
 		}
 	    }
-#endif
+
+
+	  // Allright, proceed
 
 	  proofDepth++;
 	  if (know_only)
diff --git a/src/hidelevel.c b/src/hidelevel.c
index 5541f86..bad454b 100644
--- a/src/hidelevel.c
+++ b/src/hidelevel.c
@@ -9,6 +9,8 @@
 #include "system.h"
 #include "memory.h"
 
+extern Term TERM_Hidden;
+
 //! hide level within protocol
 unsigned int
 protocolHidelevel (const System sys, const Term t)
@@ -81,6 +83,9 @@ hidelevelCompute (const System sys)
   sys->hidden = NULL;
   tl = sys->globalconstants;
 
+  // Add 'hidden' terms
+  tl = termlistAdd (tl, TERM_Hidden);
+
 #ifdef DEBUG
   if (DEBUGL (4))
     {
diff --git a/src/prune_bounds.c b/src/prune_bounds.c
index a0b0726..f6ecf5a 100644
--- a/src/prune_bounds.c
+++ b/src/prune_bounds.c
@@ -108,7 +108,7 @@ prune_bounds (const System sys)
   /**
    * This should be removed once the hidelevel lemma works correctly
    */
-  if (switches.experimental & 4)
+  if (switches.experimental & 1)
     {
       if ((switches.match < 2)
 	  && (num_intruder_runs >