---

Step * of Lemma decidable__equal_union

∀[A,B:Type].  ((∀x,y:A.  Dec(x = y ∈ A)) ⇒ (∀u,v:B.  Dec(u = v ∈ B)) ⇒ (∀x,y:A + B.  Dec(x = y ∈ (A + B))))
BY
{ (Auto THEN (D (-2)) THEN (D (-1))) }

1
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
⊢ Dec((inl x1) = (inl x) ∈ (A + B))

2
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. y1 : B
⊢ Dec((inl x1) = (inr y1 ) ∈ (A + B))

3
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))

4
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
⊢ Dec((inr y1 ) = (inr y2 ) ∈ (A + B))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    ((\mforall{}x,y:A.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}u,v:B.    Dec(u  =  v))  {}\mRightarrow{}  (\mforall{}x,y:A  +  B.    Dec(x  =  y)))


By

---

Latex:
(Auto  THEN  (D  (-2))  THEN  (D  (-1)))

---

Home Index