---

Step * 1 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. x1 : A
6. x : A
7. (inl x1) = (inl x) ∈ (A + B)
⊢ x1 = x ∈ A
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.  x1  :  A
6.  x  :  A
7.  (inl  x1)  =  (inl  x)
\mvdash{}  x1  =  x


By

---

Latex:
Obvious\mcdot{}

---

Home Index