Logical Investigations, with the Nuprl Proof Assistant  ## Theorem 17a: (C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))

∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))) Extract: λf,x,c. (f c x) where f : (C ⇒ (∀x:T. (P x))) c : C

### Nuprl Proof

Proving this first transformation is straightforward and shows how to use the construction and application rules for universal quantification. As we'll see in the next theorem, proving this transformation in the reverse direction is also straightforward. Neither direction requires any additional assumptions for a constructive proof.

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