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