The existsL proof rule makes use of an existential assumption ∃x p(x)
by, instead, assuming that p(y)
holds for some fresh variable y
about which we don't know anything.
After all, if we assume ∃x p(x)
then we know that p(y)
holds for some y
but we don't know which one.
Learning resources