---

Step * of Lemma bdd_all_zero_lemma

∀P:Top. (bdd-all(0;x.P[x]) ~ tt)
BY
{ (UnivCD THENA Auto) }

1
1. P : Top@i
⊢ bdd-all(0;x.P[x]) ~ tt

---

Latex:

---

Latex:
\mforall{}P:Top.  (bdd-all(0;x.P[x])  \msim{}  tt)


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index