---

Step * 1 of Lemma decidable__equal_consensus-rcv


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
⊢ Dec(x = y ∈ (V + ({b:Id| (b ∈ A)}  × ℕ × V)))
BY
{ (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:



1.  [V]  :  Type
2.  \mforall{}v,w:V.    Dec(v  =  w)@i
3.  A  :  Id  List@i
4.  x  :  V  +  (\{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  \mBbbN{}  \mtimes{}  V)@i
5.  y  :  V  +  (\{b:Id|  (b  \mmember{}  A)\}    \mtimes{}  \mBbbN{}  \mtimes{}  V)@i
\mvdash{}  Dec(x  =  y)


By

(BLemma  `decidable\_\_equal\_union`  THEN  Try  (Trivial))

---

Home Index