---

Step * of Lemma strong-continuous-list

∀[F:Type ⟶ Type]. Continuous+(T.F[T] List) supposing Continuous+(T.F[T])
BY
{ (Unfold `so_apply` 0 THEN Auto THEN Repeat ((D 0 THEN Auto))) }

1
.....subterm..... T:t
1:n
1. F : Type ⟶ Type
2. Continuous+(T.F T)
3. X : ℕ ⟶ Type
4. x : ⋂n:ℕ. ((F (X n)) List)
⊢ x ∈ (F (⋂n:ℕ. (X n))) List

2
1. F : Type ⟶ Type
2. Continuous+(T.F T)
3. X : ℕ ⟶ Type
4. x : (F (⋂n:ℕ. (X n))) List
5. n : ℕ
⊢ x ∈ (F (X n)) List

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  Continuous+(T.F[T]  List)  supposing  Continuous+(T.F[T])


By

---

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

---

Home Index