---

Step * of Lemma decidable__equal_cs-initial

∀[V:Type]. ∀x:consensus-state3(V). Dec(x = INITIAL ∈ consensus-state3(V))
BY
{ (Auto THEN Unfolds ``cs-initial consensus-state3`` 0 THEN D -1) }

1
1. [V] : Type
2. x1 : V@i
⊢ Dec((inl x1) = (inr inr ff  ) ∈ (V + V + 𝔹))

2
1. [V] : Type
2. y : V + 𝔹@i
⊢ Dec((inr y ) = (inr inr ff  ) ∈ (V + V + 𝔹))

---

Latex:


\mforall{}[V:Type].  \mforall{}x:consensus-state3(V).  Dec(x  =  INITIAL)


By

(Auto  THEN  Unfolds  ``cs-initial  consensus-state3``  0  THEN  D  -1)

---

Home Index