---

Step * of Lemma decidable__equal_consensus-rcv

∀[V:Type]. ((∀v,w:V.  Dec(v = w ∈ V)) ⇒ (∀A:Id List. ∀x,y:consensus-rcv(V;A).  Dec(x = y ∈ consensus-rcv(V;A))))
BY
{ (Auto THEN All (Unfold `consensus-rcv`) THEN BLemma `decidable__equal_union` THEN Try (Trivial)) }

1
.....wf..... 
1. V : Type
2. ∀v,w:V.  Dec(v = w ∈ V)@i
3. A : Id List@i
4. x : V + ({b:Id| (b ∈ A)}  × ℕ × V)@i
5. y : V + ({b:Id| (b ∈ A)}  × ℕ × V)@i
⊢ {b:Id| (b ∈ A)}  × ℕ × V ∈ Type

2
1. [V] : Type
2. ∀v,w:V.  Dec(v = w ∈ V)@i
3. A : Id List@i
4. x : V + ({b:Id| (b ∈ A)}  × ℕ × V)@i
5. y : V + ({b:Id| (b ∈ A)}  × ℕ × V)@i
⊢ ∀u,v:{b:Id| (b ∈ A)}  × ℕ × V.  Dec(u = v ∈ ({b:Id| (b ∈ A)}  × ℕ × V))

---

Latex:

---

Latex:
\mforall{}[V:Type].  ((\mforall{}v,w:V.    Dec(v  =  w))  {}\mRightarrow{}  (\mforall{}A:Id  List.  \mforall{}x,y:consensus-rcv(V;A).    Dec(x  =  y)))


By

---

Latex:
(Auto  THEN  All  (Unfold  `consensus-rcv`)  THEN  BLemma  `decidable\_\_equal\_union`  THEN  Try  (Trivial))

---

Home Index