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