~dk

An outline of how to think about the existential quantifier as it is encoded in higher order type theory. — dk