∀[P,Q:ℙ].(((¬P) ∧ (¬Q)) ⇒ (¬(P ∨ Q))) Extract: λf,g. let np,nq = f in case g of inl(p) => np p | inr(q) => nq q where f : (¬P) ∧ (¬Q) g : P ∨ Q np : ¬P ≡ (P ⇒ False) nq : ¬Q ≡ (Q ⇒ False) p : P 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 ⊢ False | BY D 3 ∧ Application rule on ((¬P) ∧ (¬Q)) | 3. ¬P 4. ¬Q 5. P ∨ Q ⊢ False | BY D 5 ∨ Application rule on (P ∨ Q) |\ | 5. P | ⊢ False Subgoal 1: Show False, assuming P | | 1 BY (Unfold `not` 3 THEN D 3) ⇒ Application rule on (P ⇒ False) | |\ | | 3. ¬Q | | 4. P | | ⊢ P Subgoal 1.1: Prove P | | | 1 2 BY NthHyp 4 Hypothesis rule | \ | 3. ¬Q | 4. P | 5. False | ⊢ False Subgoal 1.2: Show False, with assumption of False now available | | 1 BY NthHyp 5 Hypothesis rule \ 5. Q ⊢ False Subgoal 2: Show False, assuming Q | BY (Unfold `not` 4 THEN D 4) ⇒ Application rule on (Q ⇒ False) |\ | 4. Q | ⊢ Q Subgoal 2.1: Prove Q | | 1 BY NthHyp 4 Hypothesis rule \ 4. Q 5. False ⊢ False Subgoal 2.2: Show False, with assumption of False now available | BY NthHyp 5 Hypothesis rule