---

Step * of Lemma pv11_p1_eq_bnums-assert

∀[x,y:pv11_p1_Ballot_Num()].  uiff(↑(pv11_p1_eq_bnums() x y);x = y ∈ pv11_p1_Ballot_Num())
BY
{ ProveEmlLemma }

---

Latex:

---

Latex:
\mforall{}[x,y:pv11\_p1\_Ballot\_Num()].    uiff(\muparrow{}(pv11\_p1\_eq\_bnums()  x  y);x  =  y)


By

---

Latex:
ProveEmlLemma

---

Home Index