---

Step * of Lemma cs-committed-val_wf

∀[V:Type]. ∀[x:{x:consensus-state3(V)| ↑cs-is-committed(x)} ].  (cs-committed-val(x) ∈ V)
BY
{ (Unfolds ``consensus-state3 cs-is-committed cs-committed-val`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[V:Type].  \mforall{}[x:\{x:consensus-state3(V)|  \muparrow{}cs-is-committed(x)\}  ].    (cs-committed-val(x)  \mmember{}  V)


By

---

Latex:
(Unfolds  ``consensus-state3  cs-is-committed  cs-committed-val``  0  THEN  Auto)

---

Home Index