Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 17b: (∀x:T. (C ⇒ (P x))) ⇒ (C ⇒ (∀x:T. (P x)))


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

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 0 THENA Auto) ∀ Construction rule | 6. x: T ⊢ P x | BY (SimpleInstHyp ⌈x⌉ 4 THENA Auto) ∀ Application rule on | (∀x:T. (C ⇒ (P x))), using x | 7. C ⇒ (P x) ⊢ P x | BY D 7 ⇒ Application rule on (C ⇒ (P x)) |\ | ⊢ C Subgoal 1: Prove C | | 1 BY NthHyp 5 Hypothesis rule \ 7. P x ⊢ P x Subgoal 2: Prove (P x), with evidence for (P x) now available | BY NthHyp 7 Hypothesis rule




Previous Page Next Page


Table of Contents