---

       # MATH introduce existential quantifier
       # really need to link with sets for true correctness
       # and the examples here are REALLY sparse, need much more
[hear] (not / = 5 (* 2 2));

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

[hear] (not / = 3 (* 2 2));

[hear] (not / = 2 (* 2 2));

[hear] (not / = 1 (* 2 2));

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

[hear] (intro exists);

[hear] (exists (? x / = (x) (* 2 2)));

[hear] (not / = 5 (+ 5 2));

[hear] (not / = 4 (+ 4 2));

[hear] (not / = 3 (+ 3 2));

[hear] (not / = 2 (+ 2 2));

[hear] (not / = 1 (+ 1 2));

[hear] (not / = 0 (+ 0 2));

[hear] (not (exists (? x / = (x) (+ (x) 2))));