---

Step * 1 of Lemma project-seq_wf


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])
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  \mBbbN{}  {}\mrightarrow{}  Type
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  T[i])
4.  i  :  \mBbbN{}n
5.  i1  :  \mBbbN{}
6.  v1  :  T[i1]
7.  (s  i)  =  <i1,  v1>
\mvdash{}  (i1  =  i)  {}\mRightarrow{}  (v1  \mmember{}  T[i])


By

---

Latex:
Auto

---

Home Index