---

Step * 2 1 of Lemma squash-union-is-union-squash


1. A : Type
2. P : A ⟶ Type
3. a : A@i
4. y : P[a]@i
⊢ y ∈ ⋃a:A.P[a]
BY
{ (MemTypeCDUnion ⌜a⌝⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  Type
3.  a  :  A@i
4.  y  :  P[a]@i
\mvdash{}  y  \mmember{}  \mcup{}a:A.P[a]


By

---

Latex:
(MemTypeCDUnion  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index