---

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

∀[A:Type]. ∀[P:A ⟶ Type].  ↓⋃a:A.P[a] ≡ ⋃a:A.(↓P[a])
BY
{ (Auto THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....subterm..... T:t
1:n
1. A : Type
2. P : A ⟶ Type
3. x : ↓⋃a:A.P[a]@i
⊢ x ∈ ⋃a:A.(↓P[a])

2
.....subterm..... T:t
1:n
1. A : Type
2. P : A ⟶ Type
3. x : ⋃a:A.(↓P[a])@i
⊢ x ∈ ↓⋃a:A.P[a]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  Type].    \mdownarrow{}\mcup{}a:A.P[a]  \mequiv{}  \mcup{}a:A.(\mdownarrow{}P[a])


By

---

Latex:
(Auto  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index