---

Step * of Lemma apply-Id-alist-function

∀[x:Id]. ∀[F:Top]. ∀[L:Id List].  apply-alist(IdDeq;map(λx.<x, F[x]>;L);x) ~ inl F[x] supposing (x ∈ L)
BY
{ (InductionOnList
   THEN ((D 0 THENA Auto) THEN AutoSimpHyp Auto (-1)⋅)
   THEN (RWO "cons_member" (-1) THENA Auto)
   THEN Unfold `apply-alist` 0
   THEN Reduce 0
   THEN Fold `apply-alist` 0
   THEN Fold `eq_id` 0
   THEN AutoSplit
   THEN SplitOrHyps
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:Id].  \mforall{}[F:Top].  \mforall{}[L:Id  List].
    apply-alist(IdDeq;map(\mlambda{}x.<x,  F[x]>L);x)  \msim{}  inl  F[x]  supposing  (x  \mmember{}  L)


By

---

Latex:
(InductionOnList
  THEN  ((D  0  THENA  Auto)  THEN  AutoSimpHyp  Auto  (-1)\mcdot{})
  THEN  (RWO  "cons\_member"  (-1)  THENA  Auto)
  THEN  Unfold  `apply-alist`  0
  THEN  Reduce  0
  THEN  Fold  `apply-alist`  0
  THEN  Fold  `eq\_id`  0
  THEN  AutoSplit
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index