---

Step * 1 of Lemma free-from-atom-l_member


1. T : Type
2. L : T List
3. a : Atom1
4. i : ℕ
5. i < ||L||
6. a#L:T List
⊢ a#L[i]:T
BY
{ (Assert ⌜i ∈ {i:ℕ| i < ||L||} ⌝⋅ THEN Auto)⋅ }

1
1. T : Type
2. L : T List
3. a : Atom1
4. i : ℕ
5. i < ||L||
6. a#L:T List
7. i ∈ {i:ℕ| i < ||L||} 
⊢ a#L[i]:T

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  a  :  Atom1
4.  i  :  \mBbbN{}
5.  i  <  ||L||
6.  a\#L:T  List
\mvdash{}  a\#L[i]:T


By

---

Latex:
(Assert  \mkleeneopen{}i  \mmember{}  \{i:\mBbbN{}|  i  <  ||L||\}  \mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index