---

Step * 1 of Lemma e-union_wf


1. A : Base
2. A1 : Base
3. A = A1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
4. A ∈ Type
5. A1 ∈ Type
6. A ≡ A1
7. B : Base
8. B1 : Base
9. B = B1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
10. B ∈ Type
11. B1 ∈ Type
12. B ≡ B1
⊢ A ⋃ B ≡ A1 ⋃ B1
BY
{ (D 0 THEN (D 0 THENA Auto) THEN D -1 THEN Reduce 0) }

1
1. A : Base
2. A1 : Base
3. A = A1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
4. A ∈ Type
5. A1 ∈ Type
6. A ≡ A1
7. B : Base
8. B1 : Base
9. B = B1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
10. B ∈ Type
11. B1 ∈ Type
12. B ≡ B1
13. a1 : A
⊢ a1 ∈ A1 ⋃ B1

2
1. A : Base
2. A1 : Base
3. A = A1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
4. A ∈ Type
5. A1 ∈ Type
6. A ≡ A1
7. B : Base
8. B1 : Base
9. B = B1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
10. B ∈ Type
11. B1 ∈ Type
12. B ≡ B1
13. a1 : B
⊢ a1 ∈ A1 ⋃ B1

3
1. A : Base
2. A1 : Base
3. A = A1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
4. A ∈ Type
5. A1 ∈ Type
6. A ≡ A1
7. B : Base
8. B1 : Base
9. B = B1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
10. B ∈ Type
11. B1 ∈ Type
12. B ≡ B1
13. a1 : A1
⊢ a1 ∈ A ⋃ B

4
1. A : Base
2. A1 : Base
3. A = A1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
4. A ∈ Type
5. A1 ∈ Type
6. A ≡ A1
7. B : Base
8. B1 : Base
9. B = B1 ∈ pertype(λA,B. ((A ∈ Type) ∧ (B ∈ Type) ∧ A ≡ B))
10. B ∈ Type
11. B1 ∈ Type
12. B ≡ B1
13. a1 : B1
⊢ a1 ∈ A ⋃ B

---

Latex:

---

Latex:

1.  A  :  Base
2.  A1  :  Base
3.  A  =  A1
4.  A  \mmember{}  Type
5.  A1  \mmember{}  Type
6.  A  \mequiv{}  A1
7.  B  :  Base
8.  B1  :  Base
9.  B  =  B1
10.  B  \mmember{}  Type
11.  B1  \mmember{}  Type
12.  B  \mequiv{}  B1
\mvdash{}  A  \mcup{}  B  \mequiv{}  A1  \mcup{}  B1


By

---

Latex:
(D  0  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0)

---

Home Index