Make existentials more lazy

Timing gets worse, but it is not bad: https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=refinedc&var-branch1=master&var-commit1=4f0ad0efffb973e77de370367d0785027e5ed6cc&var-config1=build-coq.8.17.0-timing&var-branch2=time%2Flazy_ex&var-commit2=3ba9876efb0884f13fd3a01abb54cffbefa78cbb&var-config2=build-coq.8.17.0-timing&var-metric=instructions&var-group=%28%29.%2A

For Islaris, this MR even improves performance: https://coq-speed.mpi-sws.org/d/Ne7jkX6kk/coq-speed?from=1690301582547&to=1690813398415&var-metric=instructions&var-project=isla-coq&var-branch=All&var-config=All&var-group=%28%29.%2A