---

Step * of Lemma union-discrete

∀A,B:Type.  (discrete-type(A) ⇒ discrete-type(B) ⇒ discrete-type(A + B))
BY
{ (Auto
   THEN (D 0 THEN Auto)
   THEN ((GenConclTerm ⌜f x⌝⋅ THENA Auto) THEN D -2)
   THEN (GenConclTerm ⌜f y⌝⋅ THENA Auto)
   THEN D -2) }

1
1. A : Type@i'
2. B : Type@i'
3. discrete-type(A)
4. discrete-type(B)
5. f : ℝ ⟶ (A + B)@i
6. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y) ∈ (A + B)))
7. x : ℝ@i
8. y : ℝ@i
9. x1 : A@i
10. (f x) = (inl x1) ∈ (A + B)
11. x2 : A@i
12. (f y) = (inl x2) ∈ (A + B)
⊢ (inl x1) = (inl x2) ∈ (A + B)

2
1. A : Type@i'
2. B : Type@i'
3. discrete-type(A)
4. discrete-type(B)
5. f : ℝ ⟶ (A + B)@i
6. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y) ∈ (A + B)))
7. x : ℝ@i
8. y : ℝ@i
9. x1 : A@i
10. (f x) = (inl x1) ∈ (A + B)
11. y1 : B@i
12. (f y) = (inr y1 ) ∈ (A + B)
⊢ (inl x1) = (inr y1 ) ∈ (A + B)

3
1. A : Type@i'
2. B : Type@i'
3. discrete-type(A)
4. discrete-type(B)
5. f : ℝ ⟶ (A + B)@i
6. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y) ∈ (A + B)))
7. x : ℝ@i
8. y : ℝ@i
9. y1 : B@i
10. (f x) = (inr y1 ) ∈ (A + B)
11. x1 : A@i
12. (f y) = (inl x1) ∈ (A + B)
⊢ (inr y1 ) = (inl x1) ∈ (A + B)

4
1. A : Type@i'
2. B : Type@i'
3. discrete-type(A)
4. discrete-type(B)
5. f : ℝ ⟶ (A + B)@i
6. ∀x,y:ℝ.  ((x = y) ⇒ ((f x) = (f y) ∈ (A + B)))
7. x : ℝ@i
8. y : ℝ@i
9. y1 : B@i
10. (f x) = (inr y1 ) ∈ (A + B)
11. y2 : B@i
12. (f y) = (inr y2 ) ∈ (A + B)
⊢ (inr y1 ) = (inr y2 ) ∈ (A + B)

---

Latex:

---

Latex:
\mforall{}A,B:Type.    (discrete-type(A)  {}\mRightarrow{}  discrete-type(B)  {}\mRightarrow{}  discrete-type(A  +  B))


By

---

Latex:
(Auto
  THEN  (D  0  THEN  Auto)
  THEN  ((GenConclTerm  \mkleeneopen{}f  x\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2)
  THEN  (GenConclTerm  \mkleeneopen{}f  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2)

---

Home Index