minor

3 files changed, 7 insertions, 6 deletions

diff --git a/README.md b/README.md
index ba19dc9..9ae513e 100644
--- a/README.md
+++ b/README.md
@@ -109,13 +109,14 @@ pseudo-claim:
     forall x. forall y.
         (x <= y) or (y <= x);
 
-take x;
+take any x;
+
 [x <= x]
     (x <= x) or (x <= x)
 by [<= relates all];
 
 [reflexivity]
-    (x <= x)
+    forall x. (x <= x)
 by {Generalize}, [x <= x];
 ```
 (Note that existential quantification can be introduced by Vampire directly.)
diff --git a/core_pseudo_claims.py b/core_pseudo_claims.py
index c6fbd48..c5303c2 100644
--- a/core_pseudo_claims.py
+++ b/core_pseudo_claims.py
@@ -40,9 +40,9 @@ class GeneralizeClaim(Claim):
             # We can only universally quantify over a variable that is older
             # than any dependent var free in the expression, and older than any
             # var free in an assumption.
-            younger_than = min(assumption_vars
+            younger_than = max(assumption_vars
                                | (self.checker.dependent_vars & var_ids)
-                               | {self.checker.uid})
+                               | {-1})
             for var_id in sorted(var_ids):
                 if var_id <= younger_than:
                     continue
diff --git a/examples/readme.z3fc b/examples/readme.z3fc
index c6601e1..ee6a481 100644
--- a/examples/readme.z3fc
+++ b/examples/readme.z3fc
@@ -38,14 +38,14 @@ take 1 s.t.
     forall x. forall y.
         (x <= y) or (y <= x);
 
-take x;
+take any x;
 
 [x <= x]
     (x <= x) or (x <= x)
 by [<= relates all];
 
 [reflexivity]
-    (x <= x)
+    forall x. (x <= x)
 by {Generalize}, [x <= x];
 
 # Real Arithmetic Extension