---

Step * 1 of Lemma finite-type-product


1. [A] : Type
2. [B] : A ⟶ Type
3. ∃L:A List. ∀x:A. (x ∈ L)
4. ∀a:A. ∃L:B[a] List. ∀x:B[a]. (x ∈ L)
⊢ ∃L:(a:A × B[a]) List. ∀x:a:A × B[a]. (x ∈ L)
BY
{ ((RenameVar `f' (-1)) THEN (Unfolds ``all exists`` (-1)) THEN ExRepD) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. L : A List
4. ∀x:A. (x ∈ L)
5. f : a:A ⟶ (L:B[a] List × (x:B[a] ⟶ (x ∈ L)))
⊢ ∃L:(a:A × B[a]) List. ∀x:a:A × B[a]. (x ∈ L)

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  \mexists{}L:A  List.  \mforall{}x:A.  (x  \mmember{}  L)
4.  \mforall{}a:A.  \mexists{}L:B[a]  List.  \mforall{}x:B[a].  (x  \mmember{}  L)
\mvdash{}  \mexists{}L:(a:A  \mtimes{}  B[a])  List.  \mforall{}x:a:A  \mtimes{}  B[a].  (x  \mmember{}  L)


By

---

Latex:
((RenameVar  `f'  (-1))  THEN  (Unfolds  ``all  exists``  (-1))  THEN  ExRepD)

---

Home Index