# 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)));