---

Step * of Lemma apply_alist_wf

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[V:Type]. ∀[L:(T × V) List].
  apply_alist(eq;L;x) ∈ {v:V| (<x, v> ∈ L)}  supposing (x ∈ map(λa.(fst(a));L))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN GenListD (-1)
   THEN DVar `u'
   THEN All Reduce
   THEN (Unfold `apply_alist` 0 THEN Reduce 0)
   THEN (InstLemma `deq_property` [⌜T⌝;⌜eq⌝;⌜u1⌝;⌜x⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜eq u1 x⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN (D 0 THENA Auto)
   THEN D -4
   THEN Try (((RepeatFor 2 (D -1) THENA Auto) THEN MemTypeCD THEN Complete (Auto)))) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. V : Type
5. u1 : T
6. u2 : V
7. v : (T × V) List
8. apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ v)}  supposing (x ∈ map(λa.(fst(a));v))
9. x = u1 ∈ T
10. y : Unit
11. eq u1 x = inr y 
12. uiff(u1 = x ∈ T;↑(inr y ))
⊢ apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ [<u1, u2> / v])} 

2
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. V : Type
5. u1 : T
6. u2 : V
7. v : (T × V) List
8. apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ v)}  supposing (x ∈ map(λa.(fst(a));v))
9. (x ∈ map(λa.(fst(a));v))
10. y : Unit
11. eq u1 x = inr y 
12. uiff(u1 = x ∈ T;↑(inr y ))
⊢ apply_alist(eq;v;x) ∈ {v@0:V| (<x, v@0> ∈ [<u1, u2> / v])} 

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[V:Type].  \mforall{}[L:(T  \mtimes{}  V)  List].
    apply\_alist(eq;L;x)  \mmember{}  \{v:V|  (<x,  v>  \mmember{}  L)\}    supposing  (x  \mmember{}  map(\mlambda{}a.(fst(a));L))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  GenListD  (-1)
  THEN  DVar  `u'
  THEN  All  Reduce
  THEN  (Unfold  `apply\_alist`  0  THEN  Reduce  0)
  THEN  (InstLemma  `deq\_property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}u1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}eq  u1  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto)
  THEN  D  -4
  THEN  Try  (((RepeatFor  2  (D  -1)  THENA  Auto)  THEN  MemTypeCD  THEN  Complete  (Auto))))

---

Home Index