//

Logical Investigations, with the Nuprl Proof Assistant

## Theorem 19b: (∃x:T. (C ⇒ (Px))) ⇒ (C ⇒ (∃x:T. (Px)))

∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. (C ⇒ (P x))) ⇒ C ⇒ (∃x:T. (P x))) Extract: λf,c. let x,g = f in <x, g c> where f : ∃x:T. (C ⇒ (P x)) c : C g : C ⇒ (P x)

The reverse direction of the third transformation can be proved constructively without any extra assumptions, as shown in the following proof.

### Nuprl Proof

⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. (C ⇒ (P x))) ⇒ C ⇒ (∃x:T. (P x))) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. T: Type [2]. P: T → ℙ [3]. C: ℙ ⊢ (∃x:T. (C ⇒ (P x))) ⇒ C ⇒ (∃x:T. (P x)) | BY RepeatFor 2 ((D 0 THENA Auto)) ⇒ Construction rule, 2 times | 4. ∃x:T. (C ⇒ (P x)) 5. C ⊢ ∃x:T. (P x) | BY D 4 ∃ Application rule on (∃x:T. (C ⇒ (P x))) | 4. x: T 5. C ⇒ (P x) 6. C ⊢ ∃x:T. (P x) | BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x | ⊢ P x | BY D 5 ⇒ Application rule on (C ⇒ (P x)) |\ | 5. C | ⊢ C Subgoal 1: Prove C | | 1 BY NthHyp 5 Hypothesis rule \ 5. C 6. P x ⊢ P x Subgoal 2: Prove (P x), with evidence for (P x) now available | BY NthHyp 6 Hypothesis rule