---

Step * of Lemma list-continuity

∀[X:ℕ ⟶ Type]. ((⋂n:ℕ. (X[n] List)) ⊆r ((⋂n:ℕ. X[n]) List))
BY
{ (Unfold `so_apply` 0 THEN Auto THEN Repeat ((D 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. X : ℕ ⟶ Type
2. x : ⋂n:ℕ. ((X n) List)
⊢ x ∈ (⋂n:ℕ. (X n)) List

---

Latex:

---

Latex:
\mforall{}[X:\mBbbN{}  {}\mrightarrow{}  Type].  ((\mcap{}n:\mBbbN{}.  (X[n]  List))  \msubseteq{}r  ((\mcap{}n:\mBbbN{}.  X[n])  List))


By

---

Latex:
(Unfold  `so\_apply`  0  THEN  Auto  THEN  Repeat  ((D  0  THEN  Auto)))

---

Home Index