Strange logic for partial index proving

Sweating over the logic of the theorem prover, I notice it doesn't
actually bother to complete an accurate test. I can't see that it
produces an error, but I thought I would raise it, if only to share my
annoyance at the realisation of how it does things. :-(

drop table tenk;
create table tenk (col1 int);

insert into tenk select generate_series(1,10000);

create index idx1 on tenk (col1) where col1 > 1 and col1 < 10;

explain select * from tenk where col1 > 5 and col1 < -5;
QUERY PLAN
--------------------------------------------------------------------
Bitmap Heap Scan on tenk (cost=2.05..49.87 rows=50 width=4)
Recheck Cond: ((col1 > 5) AND (col1 < -5))
-> Bitmap Index Scan on idx1 (cost=0.00..2.05 rows=50 width=0)
Index Cond: ((col1 > 5) AND (col1 < -5))
(4 rows)

...thus it uses an index which does *not* match the query clause to test
the impossible condition and thus returns the correct answer of zero.
Seems fairly quick also :-)

AFAICS this is just a feature of the theorem prover and it never returns
an incorrect answer. Anybody think differently?

Best Regards, Simon Riggs