Improve iExist.

Now, it bases the type the quantifier ranges over on the goal, instead
of the witness. This works better when dealing with witnesses involving
type class constraints.
2 jobs for master
Status Job ID Name Coverage
  Test
passed #364
coq
buildjob

00:03:24

failed #344
coq
buildjob

00:03:07