---

Step * of Lemma project-seq_wf

∀[T:ℕ ⟶ Type]. ∀[n:ℕ]. ∀[s:ℕn ⟶ (i:ℕ × T[i])].  project-seq(s) ∈ i:ℕn ⟶ T[i] supposing ∀i:ℕn. ((fst((s i))) = i ∈ ℤ)
BY
{ (Auto
   THEN (FunExt THENW Auto)
   THEN (D -2 With ⌜i⌝  THENA Auto)
   THEN RepUR ``project-seq`` 0
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜s i⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0) }

1
1. T : ℕ ⟶ Type
2. n : ℕ
3. s : ℕn ⟶ (i:ℕ × T[i])
4. i : ℕn
5. i1 : ℕ
6. v1 : T[i1]
7. (s i) = <i1, v1> ∈ (i:ℕ × T[i])
⊢ (i1 = i ∈ ℤ) ⇒ (v1 ∈ T[i])

---

Latex:

---

Latex:
\mforall{}[T:\mBbbN{}  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  T[i])].
    project-seq(s)  \mmember{}  i:\mBbbN{}n  {}\mrightarrow{}  T[i]  supposing  \mforall{}i:\mBbbN{}n.  ((fst((s  i)))  =  i)


By

---

Latex:
(Auto
  THEN  (FunExt  THENW  Auto)
  THEN  (D  -2  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``project-seq``  0
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}s  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index