∀[A,B,C:ℙ]. ((A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C) Extract: λf,g,x. (g (f x)) where f : A ⇒ B g : B ⇒ C x : A

⊢ ∀[A,B,C:ℙ]. ((A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. A: ℙ [2]. B: ℙ [3]. C: ℙ ⊢ (A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C | BY RepeatFor 3 ((D 0 THENA Auto)) Construction rule, 3 times | 4. A ⇒ B 5. B ⇒ C 6. A ⊢ C | BY D 4 Application rule on (A ⇒ B) |\ | 4. B ⇒ C | 5. A | ⊢ A Subgoal 1: Prove A | | 1 BY NthHyp 5 Hypothesis rule \ 4. B ⇒ C 5. A 6. B ⊢ C Subgoal 2: Prove C, with evidence for B now available | BY D 4 Application rule on (B ⇒ C) |\ | 4. A | 5. B | ⊢ B Subgoal 2.1: Prove B | | 1 BY NthHyp 5 Hypothesis rule \ 4. A 5. B 6. C ⊢ C Subgoal 2.2: Prove C, with evidence for C now available | BY NthHyp 6 Hypothesis rule

∀[P,Q:ℙ].((P ⇒ (¬P)) ⇒ P ⇒ Q) Extract: λf,p. any (f p p) where f : P ⇒ (¬P) p : P

⊢ ∀[P,Q:ℙ]. ((P ⇒ (¬P)) ⇒ P ⇒ Q) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ (P ⇒ (¬P)) ⇒ P ⇒ Q | BY RepeatFor 2 ((D 0 THENA Auto)) Construction rule, 2 times | 3. P ⇒ (¬P) 4. P ⊢ Q | BY D 3 Application rule on (P ⇒ (¬P)) |\ | 3. P | ⊢ P Subgoal 1: Prove P | | 1 BY NthHyp 3 Hypothesis rule \ 3. P 4. ¬P ⊢ Q Subgoal 2: Prove Q, with evidence for (¬P) now available | BY Unfold `not` 4 | 4. P ⇒ False Definition of negation ⊢ Q | BY D 4 Application rule on (P ⇒ False) |\ | ⊢ P Subgoal 2.1: Prove P | | 1 BY NthHyp 3 Hypothesis rule \ 4. False ⊢ Q Subgoal 2.2: Prove Q, with the assumption of False now available | BY FalseHD 4 False elimination rule

∀[P,Q:ℙ].((¬(P ⇒ Q)) ⇒ P ⇒ (¬Q)) Extract: λf,p1,q.(f (λp2.q)) where f : ¬(P ⇒ Q) ≡ ((P ⇒ Q) ⇒ False) p1 : P q : Q p2 : P

⊢ ∀[P,Q:ℙ]. ((¬(P ⇒ Q)) ⇒ P ⇒ (¬Q)) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ (¬(P ⇒ Q)) ⇒ P ⇒ (¬Q) | BY RepeatFor 2 ((D 0 THENA Auto)) Construction rule, 2 times | 3. ¬(P ⇒ Q) 4. P ⊢ ¬Q | BY Unfold `not` 0 | ⊢ Q ⇒ False Definition of negation | BY (D 0 THENA Auto) Construction rule | 5. Q ⊢ False | BY Unfold `not` 3 | 3. (P ⇒ Q) ⇒ False Definition of negation ⊢ False | BY D 3 Application rule on ((P ⇒ Q) ⇒ False) |\ | 3. P | 4. Q | ⊢ P ⇒ Q Subgoal 1: Prove (P ⇒ Q) | | 1 BY (D 0 THENA Auto) Construction rule | | | 5. P | ⊢ Q | | 1 BY NthHyp 4 Hypothesis rule \ 3. P 4. Q 5. False ⊢ False Subgoal 2: Show False, with the assumption of False now available | BY NthHyp 5 Hypothesis rule

∀[P,Q:ℙ].(((¬P) ∨ Q) ⇒ P ⇒ Q) Extract: λf,p. case f of inl(np) => any (np p) | inr(q) => q f : (¬P) ∨ Q p : P np : ¬P ≡ (P ⇒ False) q : Q

⊢ ∀[P,Q:ℙ]. (((¬P) ∨ Q) ⇒ P ⇒ Q) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ ((¬P) ∨ Q) ⇒ P ⇒ Q | BY RepeatFor 2 ((D 0 THENA Auto)) ⇒ Construction rule, 2 times | 3. (¬P) ∨ Q 4. P ⊢ Q | BY D 3 ∨ Application rule on ((¬P) ∨ Q) |\ | 3. ¬P | ⊢ Q Subgoal 1: Prove Q, assuming (¬P) | | 1 BY (Unfold `not` 3 THEN D 3) ⇒ Application rule on (P ⇒ False) | |\ | | 3. P | | ⊢ P Subgoal 1.1: Prove P | | | 1 2 BY NthHyp 3 Hypothesis rule | \ | 3. P | 4. False | ⊢ Q Subgoal 1.2: Prove Q, with assumption of False now available | | 1 BY FalseHD 4 False elimination rule \ 3. Q ⊢ Q Subgoal 2: Prove Q, assuming Q | BY NthHyp 3 Hypothesis rule

∀[P,Q:ℙ].((P ⇒ Q) ⇒ (¬ ¬((¬P) ∨ Q))) Extract: λpq,f. (f (inl (λp.(f (inr (pq p) ))))) pq : P ⇒ Q f : ¬((¬P) ∨ Q) ≡ (((¬P) ∨ Q) ⇒ False) p : P

⊢ ∀[P,Q:ℙ]. ((P ⇒ Q) ⇒ (¬ ¬((¬P) ∨ Q))) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ (P ⇒ Q) ⇒ (¬ ¬((¬P) ∨ Q)) | BY RepeatFor 2 ((D 0 THENA Auto)) ⇒ Construction rule, 2 times | 3. P ⇒ Q 4. ¬((¬P) ∨ Q) ⊢ False | BY Duplicate 4 | 5. ¬((¬P) ∨ Q) ⊢ False | BY (Unfold `not` 5 THEN D 5) ⇒ Application rule on (((¬P) ∨ Q) ⇒ False) |\ | ⊢ (P ⇒ False) ∨ Q Subgoal 1: Prove ((P ⇒ False) ∨ Q) | | 1 BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | | | ⊢ P ⇒ False | | 1 BY (D 0 THENA Auto) ⇒ Construction rule | | | 5. P | ⊢ False | | 1 BY (Unfold `not` 4 THEN D 4) ⇒ Application rule on (((¬P) ∨ Q) ⇒ False) | |\ | | 4. P | | ⊢ (P ⇒ False) ∨ Q Subgoal 1.1: Prove ((P ⇒ False) ∨ Q) | | | 1 2 BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | | | | | ⊢ Q | | | 1 2 BY D 3 ⇒ Application rule on (P ⇒ Q) | | |\ | | | 3. P | | | ⊢ P Subgoal 1.1.1: Prove P | | | | 1 2 3 BY NthHyp 3 Hypothesis rule | | \ | | 3. P | | 4. Q | | ⊢ Q Subgoal 1.1.2: Prove Q, with evidence for Q now available | | | 1 2 BY NthHyp 4 Hypothesis rule | \ | 4. P | 5. False | ⊢ False Subgoal 1.2: Show False, with assumption of False now available | | 1 BY NthHyp 5 Hypothesis rule \ 5. False ⊢ False Subgoal 2: Show False, with assumption of False now available | BY NthHyp 5 Hypothesis rule

∀[P,Q:ℙ].(((P ⇒ Q) ∧ ((P ∨ (¬P)) ∨ Q ∨ (¬Q))) ⇒ ((¬P) ∨ Q)) Extract: λf.let pq,g = f in case g of inl(gp) => case gp of inl(p1) => inr (pq p1) | inr(np) => inl np | inr(gq) => case gq of inl(q) => inr q | inr(nq) => inl (λp2.(nq (pq p2))) where f : (P ⇒ Q) ∧ ((P ∨ (¬P)) ∨ Q ∨ (¬Q)) pq : P ⇒ Q g : (P ∨ (¬P)) ∨ Q ∨ (¬Q) gp : P ∨ (¬P) p1 : P np : ¬P ≡ (P ⇒ False) gq : Q ∨ (¬Q) q : Q nq : ¬Q ≡ (Q ⇒ False) p2 : P

⊢ ∀[P,Q:ℙ]. (((P ⇒ Q) ∧ ((P ∨ (¬P)) ∨ Q ∨ (¬Q))) ⇒ ((¬P) ∨ Q)) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ ((P ⇒ Q) ∧ ((P ∨ (¬P)) ∨ Q ∨ (¬Q))) ⇒ ((¬P) ∨ Q) | BY (D 0 THENA Auto) ⇒ Construction rule | 3. (P ⇒ Q) ∧ ((P ∨ (¬P)) ∨ Q ∨ (¬Q)) ⊢ (¬P) ∨ Q | BY D 3 ∧ Application rule on ((P ⇒ Q) ∧ ((P ∨ (¬P)) ∨ Q ∨ (¬Q))) | 3. P ⇒ Q 4. (P ∨ (¬P)) ∨ Q ∨ (¬Q) ⊢ (¬P) ∨ Q | BY D 4 ∨ Application rule on ((P ∨ (¬P)) ∨ (Q ∨ (¬Q))) |\ | 4. P ∨ (¬P) | ⊢ (¬P) ∨ Q Subgoal 1: Prove ((¬P) ∨ Q), assuming (P ∨ (¬P)) | | 1 BY D 4 ∨ Application rule on (P ∨ (¬P)) | |\ | | 4. P | | ⊢ (¬P) ∨ Q Subgoal 1.1: Prove ((¬P) ∨ Q), assuming P | | | 1 2 BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | | | | | ⊢ Q | | | 1 2 BY D 3 ⇒ Application rule on (P ⇒ Q) | | |\ | | | 3. P | | | ⊢ P Subgoal 1.1.1: Prove P | | | | 1 2 3 BY NthHyp 3 Hypothesis rule | | \ | | 3. P | | 4. Q | | ⊢ Q Subgoal 1.1.2: Prove Q, with evidence for Q now available | | | 1 2 BY NthHyp 4 Hypothesis rule | \ | 4. ¬P | ⊢ (¬P) ∨ Q Subgoal 1.2: Prove ((¬P) ∨ Q), assuming (¬P) | | 1 BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | | | ⊢ ¬P | | 1 BY NthHyp 4 Hypothesis rule \ 4. Q ∨ (¬Q) ⊢ (¬P) ∨ Q Subgoal 2: Prove ((¬P) ∨ Q), assuming (Q ∨ (¬Q)) | BY D 4 ∨ Application rule on (Q ∨ (¬Q)) |\ | 4. Q | ⊢ (¬P) ∨ Q Subgoal 2.1: Prove ((¬P) ∨ Q), assuming Q | | 1 BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | | | ⊢ Q | | 1 BY NthHyp 4 Hypothesis rule \ 4. ¬Q ⊢ (¬P) ∨ Q Subgoal 2.2: Prove ((¬P) ∨ Q), assuming (¬Q) | BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | ⊢ ¬P | BY (D 0 THENA Auto) ⇒ Construction rule; definition of negation | 5. P ⊢ False | BY D 3 ⇒ Application rule on (P ⇒ Q) |\ | 3. ¬Q | 4. P | ⊢ P Subgoal 2.2.1: Prove P | | 1 BY NthHyp 4 Hypothesis rule \ 3. ¬Q 4. P 5. Q ⊢ False Subgoal 2.2.2: Show False, with evidence for Q now available | BY (Unfold `not` 3 THEN D 3) ⇒ Application rule on (Q ⇒ False) |\ | 3. P | 4. Q | ⊢ Q Subgoal 2.2.2.1: Prove Q | | 1 BY NthHyp 4 Hypothesis rule \ 3. P 4. Q 5. False ⊢ False Subgoal 2.2.2.2: Show False, with assumption of False now available | BY NthHyp 5 Hypothesis rule

∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. True) ⇒ ((∃x:T. (P x)) ∨ C) ⇒ (∃x:T. ((P x) ∨ C))) Extract: λf,g. case g of inl(e) => let x,p = e in <x, inl p> | inr(c) => let x,true = f in <x, inr c> where f : ∃x:T. True g : (∃x:T. (P x)) ∨ C e : (∃x:T. (P x)) p : P x c : C

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

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

⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. ((P x) ∨ C)) ⇒ ((∃x:T. (P x)) ∨ C)) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. T: Type [2]. P: T → ℙ [3]. C: ℙ ⊢ (∃x:T. ((P x) ∨ C)) ⇒ ((∃x:T. (P x)) ∨ C) | BY (D 0 THENA Auto) ⇒ Construction rule | 4. ∃x:T. ((P x) ∨ C) ⊢ (∃x:T. (P x)) ∨ C | BY D 4 ∃ Application rule on (∃x:T. ((P x) ∨ C)) | 4. x: T 5. (P x) ∨ C ⊢ (∃x:T. (P x)) ∨ C | BY D 5 ∨ Application rule on ((P x) ∨ C) |\ | 5. P x | ⊢ (∃x:T. (P x)) ∨ C Subgoal 1: Prove ((∃x:T. (P x)) ∨ C), | | assuming evidence for (P x) | | 1 BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | | | ⊢ ∃x:T. (P x) | | 1 BY (InstConcl [⌈x⌉] THENA Auto) ∃ Construction rule, using x | | | ⊢ P x | | 1 BY NthHyp 5 Hypothesis rule \ 5. C ⊢ (∃x:T. (P x)) ∨ C Subgoal 2: Prove ((∃x:T. (P x)) ∨ C), | assuming evidence for C | BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | ⊢ C | BY NthHyp 5 Hypothesis rule

∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. (((∀x:T. (P x)) ∨ C) ⇒ (∀x:T. ((P x) ∨ C))) Extract: λf,x. case f of inl(g) => inl (g x) | inr(c) => inr c where f : (∀x:T. (P x)) ∨ C g : ∀x:T. (P x) c : C

⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. (((∀x:T. (P x)) ∨ C) ⇒ (∀x:T. ((P x) ∨ C))) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. T: Type [2]. P: T → ℙ [3]. C: ℙ ⊢ ((∀x:T. (P x)) ∨ C) ⇒ (∀x:T. ((P x) ∨ C)) | BY (D 0 THENA Auto) ⇒ Construction rule | 4. (∀x:T. (P x)) ∨ C ⊢ ∀x:T. ((P x) ∨ C) | BY (D 0 THENA Auto) ∀ Construction rule | 5. x: T ⊢ (P x) ∨ C | BY D 4 ∨ Application rule on ((∀x:T. (P x)) ∨ C) |\ | 4. ∀x:T. (P x) | ⊢ (P x) ∨ C Subgoal 1: Prove ((P x) ∨ C), | | assuming evidence for (∀x:T. (P x)) | | 1 BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | | | ⊢ P x | | 1 BY (SimpleInstHyp ⌈x⌉ 4 THENA Auto) ∀ Application rule on (∀x:T. (P x)), | | using x | | | 6. P x | ⊢ P x | | 1 BY NthHyp 6 Hypothesis rule \ 4. C ⊢ (P x) ∨ C Subgoal 2: Prove ((P x) ∨ C), | assuming evidence for C | BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | ⊢ C | BY NthHyp 4 Hypothesis rule

∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((C ∨ (¬C)) ⇒ (∀x:T. ((P x) ∨ C)) ⇒ ((∀x:T. (P x)) ∨ C)) Extract: λf,g. case f of inl(c) => inr c | inr(nc) => inl (λx.case g x of inl(p) => p | inr(c) => any (nc c)) where f : C ∨ (¬C) g : ∀x:T. ((P x) ∨ C) c : C nc : ¬C ≡ (C ⇒ False) p : P x

⊢ ∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. | ((C ∨ (¬C)) ⇒ (∀x:T. ((P x) ∨ C)) ⇒ ((∀x:T. (P x)) ∨ C)) | BY RepeatFor 3 ((UD THENA Auto)) | [1]. T: Type [2]. P: T → ℙ [3]. C: ℙ ⊢ (C ∨ (¬C)) ⇒ (∀x:T. ((P x) ∨ C)) ⇒ ((∀x:T. (P x)) ∨ C) | BY RepeatFor 2 ((D 0 THENA Auto)) ⇒ Construction rule, 2 times | 4. C ∨ (¬C) 5. ∀x:T. ((P x) ∨ C) ⊢ (∀x:T. (P x)) ∨ C | BY D 4 ∨ Application rule on (C ∨ (¬C)) |\ | 4. C | ⊢ (∀x:T. (P x)) ∨ C Subgoal 1: Prove ((∀x:T. (P x)) ∨ C), | | assuming evidence for C | | 1 BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | | | ⊢ C | | 1 BY NthHyp 4 Hypothesis rule \ 4. ¬C ⊢ (∀x:T. (P x)) ∨ C Subgoal 2: Prove ((∀x:T. (P x)) ∨ C), | assuming evidence for (¬C) | BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | ⊢ ∀x:T. (P x) | BY (D 0 THENA Auto) ∀ Construction rule | 6. x: T ⊢ P x | BY (SimpleInstHyp ⌈x⌉ 5 THENA Auto) ∀ Application rule on | (∀x:T. ((P x) ∨ C)), using x | 7. (P x) ∨ C ⊢ P x | BY D 7 ∨ Application rule on ((P x) ∨ C) |\ | 7. P x | ⊢ P x Subgoal 2.1: Prove (P x), assuming evidence for (P x) | | 1 BY NthHyp 7 Hypothesis rule \ 7. C ⊢ P x Subgoal 2.2: Prove (P x), assuming evidence for C | BY (Unfold `not` 4 THEN D 4) ⇒ Application rule on (C ⇒ False) |\ | 4. ∀x:T. ((P x) ∨ C) | 5. x: T | 6. C | ⊢ C Subgoal 2.2.1: Prove C | | 1 BY NthHyp 6 Hypothesis rule \ 4. ∀x:T. ((P x) ∨ C) 5. x: T 6. C 7. False ⊢ P x Subgoal 2.2.2: Prove (P x), with assumption of False now available | BY FalseHD 7 False elimination rule

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

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

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

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

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

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

∀[T:Type]. ∀[P:T → ℙ]. ∀[C:ℙ]. ((∃x:T. True) ⇒ (∀x:T. ((P x) ∧ C)) ⇒ ((∀x:T. (P x)) ∧ C)) Extract: λe,f. <λx.let p1,c1 = f x in p1, let x,true = e in let p2,c2 = f x in c2> where e : ∃x:T. True f : ∀x:T. ((P x) ∧ C) p1 : P x c1 : C p2 : P x c2 : C

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