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