---

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

.....subterm..... T:t
1:n
1. A : Type
2. P : A ⟶ Type
3. x : ⋃a:A.(↓P[a])@i
⊢ x ∈ ↓⋃a:A.P[a]
BY
{ (D_union (-1)
   THEN (D (-1) THEN RenameVar `y' (-1))
   THEN Unfold `squash` 0
   THEN MemCDImageType⋅
   THEN Fold `member` 0
   THEN Auto) }

1
1. A : Type
2. P : A ⟶ Type
3. a : A@i
4. y : P[a]@i
⊢ y ∈ ⋃a:A.P[a]

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  Type
3.  x  :  \mcup{}a:A.(\mdownarrow{}P[a])@i
\mvdash{}  x  \mmember{}  \mdownarrow{}\mcup{}a:A.P[a]


By

---

Latex:
(D\_union  (-1)
  THEN  (D  (-1)  THEN  RenameVar  `y'  (-1))
  THEN  Unfold  `squash`  0
  THEN  MemCDImageType\mcdot{}
  THEN  Fold  `member`  0
  THEN  Auto)

---

Home Index