∀[A,B: ℙ]. {(A ∨ B) ⇔ ¬(¬A ∧ ¬B)} {(A ∨ B) ⇒ ¬(¬A ∧ ¬B)} ⇒ Extract: λf.λg.spread(g; na,nb.decide(f;a.ap(na.a);b.ap(nb.b))

A ∨ B ⇒ ¬(¬A ∧ ¬B)	by λ(f.___)
f : A ∨ B ⊢ ¬(¬A ∧ ¬B)	by λ(g.____)
f : A ∨ B, g: ¬A ∧ ¬B ⊢ False	by spread(g; na,nb.___)
f : A ∨ B, na : ¬A, nb : ¬B ⊢ False	by decide(f;a. slot1 ; b. slot2 )
a : A B, na : ¬A, nb : ¬B ⊢ False	by ap(na.a) for slot1
b : B, na : ¬A, nb : ¬B ⊢ False	by ap(nb.b) for slot2

{¬(¬A ∧ ¬B) ⇒ (A ∨ B)} ⇐ Extract: λf.(CC;g.any(ap(f.<λa.ap(g.inl(a));λb.ap(g.inr(b))>)))

{¬(¬A ∧ ¬B) ⇒ A ∨ B}	by λ(f.___)
f : ¬(¬A ∧ ¬B) ⊢ {A ∨ B}	by (CC{A ∨ B};g.___) Classical contradiction
f : ¬(¬A ∧ ¬B), g : ¬(A ∨ B) ⊢ {A ∨ B}	by apseq(f;____;False.any(..))
g : ¬(A ∨ B) ⊢ ¬A ∧ ¬B	by pair( slot1 ; slot2 )
g : ¬(A ∨ B) ⊢ ¬A	by λ(a.___) for slot1
g : ¬(A ∨ B), a : A ⊢ False	by ap(g.___)
a : A ⊢ A ∨ B	by inl(___)
a : A ⊢ A	by a
naob : ¬(A ∨ B) ⊢ ¬B	by λ(b.___) for slot2
naob : ¬(A ∨ B), b : B ⊢ False	by ap(g.___)
b : B ⊢ A ∨ B	by inr(___)
b : B ⊢ B	by b

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