Set F0 to be the term
λX ⇒ pack_u (int ⨯ X) (λu ⇒ (u 0 + 1,u 1)) of type
set → set.
Set F1 to be the term
λX Y h ⇒ λu ∈ int ⨯ X ⇒ (u 0,h (u 1)) of type
set → set → set → set.
Set eta to be the term
λX ⇒ λx ∈ X ⇒ (0,x) of type
set → set.
Set eps to be the term
λA ⇒ unpack_u_i A epsPhi of type
set → set.
We use F0 to witness the existential quantifier.
We use F1 to witness the existential quantifier.
We use eta to witness the existential quantifier.
We use eps to witness the existential quantifier.
∎