---

Step * 3 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. x : A
⊢ Dec((inr y1 ) = (inl x) ∈ (A + B))
BY
{ (Unfold `decidable` 0 THEN OrRight THEN Auto THEN 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.  x  :  A
\mvdash{}  Dec((inr  y1  )  =  (inl  x))


By

---

Latex:
(Unfold  `decidable`  0  THEN  OrRight  THEN  Auto  THEN  Obvious)

---

Home Index