---

Step * 1 of Lemma consensus-state2-cases

.....equality..... 
1. V : Type
2. y1 : Top@i
⊢ (inr inr y1  ) = AMBIVALENT ∈ consensus-state2(V)
BY
{ (Unfolds ``cs-ambivalent consensus-state2`` 0 THEN Auto) }

---

Latex:


.....equality..... 
1.  V  :  Type
2.  y1  :  Top@i
\mvdash{}  (inr  inr  y1    )  =  AMBIVALENT


By

(Unfolds  ``cs-ambivalent  consensus-state2``  0  THEN  Auto)

---

Home Index