---

Step * of Lemma apply-alist-no_repeats

∀[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[L:(T × A) List].
  ∀[x:T]. ∀[a:A].  apply-alist(eq;L;x) = (inl a) ∈ (A?) supposing (<x, a> ∈ L) 
  supposing no_repeats(T;map(λp.(fst(p));L))
BY
{ ((Auto THEN (InstLemma `apply-alist-cases` [⌜T⌝;⌜eq⌝;⌜x⌝;⌜L⌝]⋅ THENA Auto))
   THEN RepeatFor 2 (D -2)
   THEN D -1
   THEN InstHyp [⌜i⌝] (-1)⋅
   THEN Auto) }

1
1. A : Type
2. T : Type
3. eq : EqDecider(T)
4. L : (T × A) List
5. no_repeats(T;map(λp.(fst(p));L))
6. x : T
7. a : A
8. i : ℕ
9. i < ||L||
10. <x, a> = L[i] ∈ (T × A)
11. apply-alist(eq;L;x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));L))
12. ∀[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))))
13. j : ℕi
⊢ ¬((fst(L[j])) = x ∈ T)

2
1. A : Type
2. T : Type
3. eq : EqDecider(T)
4. L : (T × A) List
5. no_repeats(T;map(λp.(fst(p));L))
6. x : T
7. a : A
8. i : ℕ
9. i < ||L||
10. <x, a> = L[i] ∈ (T × A)
11. apply-alist(eq;L;x) ~ ff supposing ¬(x ∈ map(λp.(fst(p));L))
12. ∀[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))))
13. apply-alist(eq;L;x) ~ inl (snd(L[i]))
⊢ apply-alist(eq;L;x) = (inl a) ∈ (A?)

---

Latex:

---

Latex:
\mforall{}[A,T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[L:(T  \mtimes{}  A)  List].
    \mforall{}[x:T].  \mforall{}[a:A].    apply-alist(eq;L;x)  =  (inl  a)  supposing  (<x,  a>  \mmember{}  L) 
    supposing  no\_repeats(T;map(\mlambda{}p.(fst(p));L))


By

---

Latex:
((Auto  THEN  (InstLemma  `apply-alist-cases`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  RepeatFor  2  (D  -2)
  THEN  D  -1
  THEN  InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index