∀[A,B: ℙ]. {A ∨ B ∨ ¬B ⇔ B ∨ ¬ B} {(B ∨ ¬B) ⇒ (A ∨ B ∨ ¬B)} ⇐ Extract: λf.inr(f)

B ∨ ¬B ⇒ A ∨ B ∨ ¬B	by λ(f.___)
bonb : B ∨ ¬B ⊢ A ∨ B ∨ ¬B	by inr(___)
bonb : B ∨ ¬B ⊢ B ∨ ¬B	by f

{(A ∨ B ∨ ¬B) ⇒ (B ∨ ¬B)} ⇒ Extract: λf.(CC;g.inr(λb.ap(g.inl(b))))

{A ∨ B ∨ ¬B ⇒ B ∨ ¬B}	by λ(f.___)
f : A ∨ B ∨ ¬B ⊢ {B ∨ ¬B}	by (CC{B ∨ ¬B};g.___) Classical contradiction
f : A ∨ B ∨ ¬B, g : ¬(B ∨ ¬B) ⊢ {B ∨ ¬B}	by inr(___)
f : A ∨ B ∨ ¬B, g : ¬(B ∨ ¬B) ⊢ {¬B}	by λ(b.____)
f : A ∨ B ∨ ¬B, g : ¬(B ∨ ¬B), b : B ⊢ False	by ap(g.___)
f : A ∨ B ∨ ¬B, b : B ⊢ B ∨ ¬B	by inl(___)
f : A ∨ B ∨ ¬B, b : B ⊢ B	by b

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