---

Step * of Lemma apply-alist-function

∀[T,A:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[F:T ⟶ A]. ∀[L:T List].
  apply-alist(eq;map(λx.<x, F[x]>;L);x) = (inl F[x]) ∈ (A?) supposing (x ∈ L)
BY
{ ((InductionOnList THEN Auto)
   THEN ((RWO "cons_member" (-1) THENA Auto)
         THEN Unfold `apply-alist` 0
         THEN Reduce 0
         THEN Fold `apply-alist` 0
         THEN AutoSplit
         THEN (BackThruSomeHyp THEN D (-1) THEN Auto THEN D (-4) THEN Auto)⋅)⋅
   ) }

---

Latex:

---

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


By

---

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

---

Home Index