The proof now works on all applications, not just chains that start with
an Inj.

Cleaned up the valid-predicate. It is much less cluttered now and does
the same thing. I added an example to show how it works.

There are still several admits, and the 'easier' case where no
quantifiers are pulled has still to be done.