---

       # MATH introduce universal quantifier
       # really need to link with sets for true correctness
       # and the examples here are REALLY sparse, need much more
[hear] (intro forall);

[hear] (< 5 (+ 5 1));

[hear] (< 4 (+ 4 1));

[hear] (< 3 (+ 3 1));

[hear] (< 2 (+ 2 1));

[hear] (< 1 (+ 1 1));

[hear] (< 0 (+ 0 1));

[hear] (forall (? x / < (x) (+ (x) 1)));

[hear] (< 5 (* 5 2));

[hear] (< 4 (* 4 2));

[hear] (< 3 (* 3 2));

[hear] (< 2 (* 2 2));

[hear] (< 1 (* 1 2));

[hear] (not / < 0 (* 0 2));

[hear] (not / forall (? x / < (x) (* (x) 2)));