---

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?)
BY
{ (InductionOnList THEN ProveWfLemma THEN Reduce 0 THEN Auto THEN Fold `apply-alist` 0 THEN Auto) }

---

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?)


By

---

Latex:
(InductionOnList  THEN  ProveWfLemma  THEN  Reduce  0  THEN  Auto  THEN  Fold  `apply-alist`  0  THEN  Auto)

---

Home Index