---

Step * of Lemma not-not-1-xmiddle

No Annotations
∀[P:ℙ]. (¬¬(P ∨ (¬P)))
BY
{ ((InstLemma `minimal-not-not-xmiddle` [] THEN ParallelLast THEN (D -1 With ⌜False⌝  THENA Auto))
   THEN Fold `not` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[P:\mBbbP{}].  (\mneg{}\mneg{}(P  \mvee{}  (\mneg{}P)))


By

---

Latex:
((InstLemma  `minimal-not-not-xmiddle`  []  THEN  ParallelLast  THEN  (D  -1  With  \mkleeneopen{}False\mkleeneclose{}    THENA  Auto))
  THEN  Fold  `not`  (-1)
  THEN  Trivial)

---

Home Index