---

Step * of Lemma non-uniform-triple-neg-ext

∀A:ℙ. (¬¬¬A ⇐⇒ ¬A)
BY
{ Extract of Obid: non-uniform-triple-neg
  normalizes to:
  
  λA.<λh,x. Ax, λh,x. Ax>
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}A:\mBbbP{}.  (\mneg{}\mneg{}\mneg{}A  \mLeftarrow{}{}\mRightarrow{}  \mneg{}A)


By

---

Latex:
Extract  of  Obid:  non-uniform-triple-neg
normalizes  to:

\mlambda{}A.<\mlambda{}h,x.  Ax,  \mlambda{}h,x.  Ax>
finishing  with  Auto

---

Home Index