---

Step * 1 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
7. i ∈ {i:ℕ| i < ||L||} 
⊢ a#L[i]:T
BY
{ (FreeFromAtomApElim ⌜i⌝⋅ THEN Try (FreeFromAtomApElim ⌜L⌝⋅) THEN FreeFromAtomSet THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
(FreeFromAtomApElim  \mkleeneopen{}i\mkleeneclose{}\mcdot{}  THEN  Try  (FreeFromAtomApElim  \mkleeneopen{}L\mkleeneclose{}\mcdot{})  THEN  FreeFromAtomSet  THEN  Auto)

---

Home Index