∀[A,B: ℙ]. {(~A ⇒ B) ⇒ ~B ⇒ A} Extract: λf.λnb.(CC;na.any(ap(nb.ap(f.na))))

{(¬A ⇒ B) ⇒ (¬B) ⇒ A}	by λ(f.___)
f : ¬A ⇒ B ⊢ {¬B ⇒ A}	by λ(nb.___)
f : ¬A ⇒ B, nb : ¬B ⊢ {A}	by (CC{A};na.____) Classical contradiction
f : ¬A ⇒ B, nb : ¬B, na : ¬A ⊢ {A}	by apseq(nb;___;False.any(..))
f : ¬A ⇒ B, na : ¬A ⊢ B	by ap(f.___)
na : ¬A ⊢ ¬A	by na

⊢ ∀[A,B:ℙ]. {(¬A ⇒ B) ⇒ (¬B) ⇒ A} | BY (D 0 THENA Auto) |\ | 1. A: ℙ | ⊢ ∀[B:ℙ]. {((¬A) ⇒ B) ⇒ (¬B) ⇒ A} | | 1 BY (D 0 THENA Auto) | |\ | | 2. B: ℙ | | ⊢ {((¬A) ⇒ B) ⇒ (¬B) ⇒ A} | | | 1 2 BY RepeatFor 4 ((D 0 THENA Auto)) | | | | | 3. (¬A) ⇒ B | | 4. ¬B | | ⊢ {A} | | | 1 2 BY (ClassicalContradiction THENA Auto) Add contradiction of goal to hypotheses | | | | | 5. ¬A | | ⊢ {A} | | | 1 2 BY D 3 | | |\ | | | 3. ¬B | | | 4. ¬A | | | ⊢ ¬A | | | | 1 2 3 BY Hypothesis | | \ | | 3. ¬B | | 4. ¬A | | 5. B | | ⊢ {A} | | | 1 2 BY D 3 | | | | | 3. ¬A | | 4. B | | ⊢ B | | | 1 2 BY Hypothesis | \ | 2. B: ℙ | 3. {x:Unit| ((¬A) ⇒ B) ⇒ (¬B) ⇒ A} | ⊢ Ax ∈ {x:Unit| ((¬A) ⇒ B) ⇒ (¬B) ⇒ A} | | 1 BY Auto \ 1. A: ℙ 2. B: ℙ 3. {x:Unit| ((¬A) ⇒ B) ⇒ (¬B) ⇒ A} ⊢ Ax ∈ {x:Unit| ((¬A) ⇒ B) ⇒ (¬B) ⇒ A} | BY Auto PDF version of proof