---

Step * of Lemma apply-alist-cases

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:(T × Top) List].
  (apply-alist(eq;L;x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));L))
  ∧ (∀[i:ℕ||L||]
       (apply-alist(eq;L;x) ~ inl (snd(L[i]))) supposing (((fst(L[i])) = x ∈ T) and (∀j:ℕi. (¬((fst(L[j])) = x ∈ T))))))
BY
{ InductionOnList }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
⊢ apply-alist(eq;[];x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));[]))
∧ (∀[i:ℕ||[]||]
     (apply-alist(eq;[];x) ~ inl (snd([][i]))) supposing (((fst([][i])) = x ∈ T) and (∀j:ℕi. (¬((fst([][j])) = x ∈ T))))\000C)

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. u : T × Top
5. v : (T × Top) List
6. apply-alist(eq;v;x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));v))
∧ (∀[i:ℕ||v||]
     (apply-alist(eq;v;x) ~ inl (snd(v[i]))) supposing (((fst(v[i])) = x ∈ T) and (∀j:ℕi. (¬((fst(v[j])) = x ∈ T)))))
⊢ apply-alist(eq;[u / v];x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));[u / v]))
∧ (∀[i:ℕ||[u / v]||]
     (apply-alist(eq;[u / v];x) ~ inl (snd([u / v][i]))) supposing 
        (((fst([u / v][i])) = x ∈ T) and 
        (∀j:ℕi. (¬((fst([u / v][j])) = x ∈ T)))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[L:(T  \mtimes{}  Top)  List].
    (apply-alist(eq;L;x)  \msim{}  ff  supposing  \mneg{}(x  \mmember{}  map(\mlambda{}p.(fst(p));L))
    \mwedge{}  (\mforall{}[i:\mBbbN{}||L||]
              (apply-alist(eq;L;x)  \msim{}  inl  (snd(L[i])))  supposing 
                    (((fst(L[i]))  =  x)  and 
                    (\mforall{}j:\mBbbN{}i.  (\mneg{}((fst(L[j]))  =  x))))))


By

---

Latex:
InductionOnList

---

Home Index