A single witness working for every object supplies a witness for each object individually. Eliminate the outer existential with a fresh witness, instantiate the universal at an arbitrary object, and introduce the required existential. Generalization can occur either before or after closing the witness scope, provided the eigenvariable condition holds in the corresponding contexts. The converse fails on a two-element domain with interpreted as equality: each object has itself as a witness, but no object works for both.

Articles by others on the same topic (0)

There are currently no matching articles.