---

Step * 2 2 of Lemma Peirce-subtype-dneg-elim


1. P : ℙ
2. x : ∀[B:ℙ]. (((P ⇒ B) ⇒ P) ⇒ P)
3. x = x ∈ (((P ⇒ Void) ⇒ P) ⇒ P)
⊢ (((P ⇒ Void) ⇒ P) ⇒ P) ⊆r ((¬¬P) ⇒ P)
BY
{ (All Thin THEN (D 0 THENA Auto)) }

1
.....subterm..... T:t
1:n
1. P : ℙ
2. x : ((P ⇒ Void) ⇒ P) ⇒ P
⊢ x ∈ (¬¬P) ⇒ P

---

Latex:

---

Latex:

1.  P  :  \mBbbP{}
2.  x  :  \mforall{}[B:\mBbbP{}].  (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P)
3.  x  =  x
\mvdash{}  (((P  {}\mRightarrow{}  Void)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P)  \msubseteq{}r  ((\mneg{}\mneg{}P)  {}\mRightarrow{}  P)


By

---

Latex:
(All  Thin  THEN  (D  0  THENA  Auto))

---

Home Index