---

Step * of Lemma Peirce-subtype-dneg-elim

(∀[P,B:ℙ].  (((P ⇒ B) ⇒ P) ⇒ P)) ⊆r (∀[P:ℙ]. ((¬¬P) ⇒ P))
BY
{ ((D 0 THENA Auto)
   THEN (Unfold `uall` 0 THEN (MemTypeCD THENA Auto))
   THEN SubsumeC ⌜∀[B:ℙ]. (((P ⇒ B) ⇒ P) ⇒ P)⌝⋅) }

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

2
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)

---

Latex:

---

Latex:
(\mforall{}[P,B:\mBbbP{}].    (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P))  \msubseteq{}r  (\mforall{}[P:\mBbbP{}].  ((\mneg{}\mneg{}P)  {}\mRightarrow{}  P))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Unfold  `uall`  0  THEN  (MemTypeCD  THENA  Auto))
  THEN  SubsumeC  \mkleeneopen{}\mforall{}[B:\mBbbP{}].  (((P  {}\mRightarrow{}  B)  {}\mRightarrow{}  P)  {}\mRightarrow{}  P)\mkleeneclose{}\mcdot{})

---

Home Index