---

Step * 1 1 of Lemma member_map


1. [T] : Type
2. [T'] : Type
3. a : T List
4. x : T'
5. f : T ⟶ T'
6. i : ℕ
7. i < ||a||
8. x = (f a[i]) ∈ T'
⊢ ∃y:T. ((∃i:ℕ. (i < ||a|| c∧ (y = a[i] ∈ T))) ∧ (x = (f y) ∈ T'))
BY
{ (InstConcl [a[i]] THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [T']  :  Type
3.  a  :  T  List
4.  x  :  T'
5.  f  :  T  {}\mrightarrow{}  T'
6.  i  :  \mBbbN{}
7.  i  <  ||a||
8.  x  =  (f  a[i])
\mvdash{}  \mexists{}y:T.  ((\mexists{}i:\mBbbN{}.  (i  <  ||a||  c\mwedge{}  (y  =  a[i])))  \mwedge{}  (x  =  (f  y)))


By

---

Latex:
(InstConcl  [a[i]]  THEN  Auto)

---

Home Index