---

Step * 4 1 of Lemma decidable__equal_union


1. A : Type
2. B : Type
3. ∀x,y:A.  Dec(x = y ∈ A)
4. ∀u,v:B.  Dec(u = v ∈ B)
5. y1 : B
6. y2 : B
7. (inr y1 ) = (inr y2 ) ∈ (A + B)
⊢ y1 = y2 ∈ B
BY
{ Obvious }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  \mforall{}x,y:A.    Dec(x  =  y)
4.  \mforall{}u,v:B.    Dec(u  =  v)
5.  y1  :  B
6.  y2  :  B
7.  (inr  y1  )  =  (inr  y2  )
\mvdash{}  y1  =  y2


By

---

Latex:
Obvious

---

Home Index