---

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


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

1
1. P : ℙ
2. x : ∀[B:ℙ]. (((P ⇒ B) ⇒ P) ⇒ P)
⊢ x ∈ ((P ⇒ Void) ⇒ P) ⇒ P

2
1. P : ℙ
2. x : ∀[B:ℙ]. (((P ⇒ B) ⇒ P) ⇒ P)
3. x = x ∈ (((P ⇒ Void) ⇒ P) ⇒ P)
⊢ (((P ⇒ Void) ⇒ P) ⇒ P) ⊆r ((¬¬P) ⇒ P)

---

Latex:

---

Latex:

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


By

---

Latex:
(All  Thin  THEN  (D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}((P  {}\mRightarrow{}  Void)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P\mkleeneclose{}\mcdot{})

---

Home Index