---

Step * of Lemma not-not-assert

∀[b:𝔹]. uiff(¬¬↑b;↑b)
BY
{ (Auto THEN Try ((D 0 THEN Complete (Auto)))) }

1
1. b : 𝔹
2. ¬¬↑b
⊢ ↑b

---

Latex:

---

Latex:
\mforall{}[b:\mBbbB{}].  uiff(\mneg{}\mneg{}\muparrow{}b;\muparrow{}b)


By

---

Latex:
(Auto  THEN  Try  ((D  0  THEN  Complete  (Auto))))

---

Home Index