---

Step * 1 4 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
13. a1 : B1
⊢ a1 ∈ A ⋃ B
BY
{ (SubsumeC ⌜B⌝⋅ THEN Auto) }

---

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
13.  a1  :  B1
\mvdash{}  a1  \mmember{}  A  \mcup{}  B


By

---

Latex:
(SubsumeC  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index