---

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

.....subterm..... T:t
1:n
1. T : Type
2. P : T ⟶ ℙ
3. x : ⋃x:T.(↓P[x])@i
⊢ x ∈ ↓∃x:T. P[x]
BY
{ (D_union (-1)
   THEN D (-1)
   THEN (RenameVar `y' (-1) THEN Subst' (λx.Ax) y ~ (λx.Ax) <x, y> 0)
   THEN Try ((Unfold `squash` 0 THEN MemCDImageType⋅ THEN (Fold `member` 0 THEN Auto)))) }

1
.....equality..... 
1. T : Type
2. P : T ⟶ ℙ
3. x : T@i
4. y : P[x]@i
⊢ (λx.Ax) y ~ (λx.Ax) <x, y>

---

Latex:

---

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


By

---

Latex:
(D\_union  (-1)
  THEN  D  (-1)
  THEN  (RenameVar  `y'  (-1)  THEN  Subst'  (\mlambda{}x.Ax)  y  \msim{}  (\mlambda{}x.Ax)  <x,  y>  0)
  THEN  Try  ((Unfold  `squash`  0  THEN  MemCDImageType\mcdot{}  THEN  (Fold  `member`  0  THEN  Auto))))

---

Home Index