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

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

⊢ ∀[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 5 | | | | | ⊢ 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