---

Step * of Lemma triple-neg-ext

∀[A:ℙ]. uiff(¬¬¬A;¬A)
BY
{ Extract of Obid: triple-neg
  normalizes to:
  
  <λv.Ax, λv.Ax>
  finishing with Auto }

---

Latex:

---

Latex:
\mforall{}[A:\mBbbP{}].  uiff(\mneg{}\mneg{}\mneg{}A;\mneg{}A)


By

---

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

<\mlambda{}v.Ax,  \mlambda{}v.Ax>
finishing  with  Auto

---

Home Index