---

Step * of Lemma free-from-atom-l_member

∀[T:Type]. ∀[L:T List]. ∀[a:Atom1]. ∀[x:T].  (a#x:T) supposing (a#L:T List and (x ∈ L))
BY
{ (Repeat (D 0 THENA Complete Auto)
   THEN At ⌜Type⌝ Auto⋅
   THEN (RepeatFor 3 (D -2) THEN At ⌜Type⌝ (HypSubst' -2 0)⋅ THEN Auto THEN ThinVar `x')⋅) }

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[a:Atom1].  \mforall{}[x:T].    (a\#x:T)  supposing  (a\#L:T  List  and  (x  \mmember{}  L))


By

---

Latex:
(Repeat  (D  0  THENA  Complete  Auto)
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  Auto\mcdot{}
  THEN  (RepeatFor  3  (D  -2)  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (HypSubst'  -2  0)\mcdot{}  THEN  Auto  THEN  ThinVar  `x')\mcdot{})

---

Home Index